structures, subtypes, coercions and rw

Stream: new members

[Antoine Chambert-Loir]

I have two questions that puzzle me.
The context is similar in both, a group G acting on a type X:

variables {G:Type*} [group G] {X:Type*} [mul_action G X]

1) The first one is about is_pretransitive, defined as a structure.
Assume I have H: subgroup G and the hypothesis h: is_pretransitive ↥H X (meaning that Hacts pretransitively on X), as well as two members x y : X.
I want to recover the defining property of is_pretransitive, exists_smul_eq, which expands as ∀ (x y : X), ∃ (g : ↥H), g • x = y, and apply it to xand y, to recover g, but while the following

let z := h.exists_smul_eq,
obtain ⟨g,h⟩ := z x y,

gives me what I want, namely, g: ↥H and h: g • x = y, the following

obtain ⟨g,h⟩ := h.exists_smul_eq x y,

returns a cryptic

    invalid field notation,
function 'mul_action.is_pretransitive.exists_smul_eq' does not have explicit argument
with type (mul_action.is_pretransitive ...)

2) Anyway, at that point, I arrive at the following context,

x y:  X
g: ↥H
hgxy: g • x = y
z': T (↑g • x) = ⇑mul_aut.conj ↑g • T x
⊢ T (g • x) ≤ H ⊔ T x

but I get coercions ↑g that prevent me to rw z'. Can you explain me what I did wrong, or what goes on?
Thank you !

[Ruben Van de Velde]

Can you paste a #mwe? Then people can start playing with the code

[Yaël Dillies]

I think I got it. Don't worry, Ruben.

[Adam Topaz]

This works for me:

import group_theory.group_action.basic

variables (G X : Type*) [group G] [mul_action G X] (H : subgroup G)
  [mul_action.is_pretransitive H X]

include G X H

example : mul_action H X := infer_instance

example (x y : X) : true :=
begin
  obtain ⟨g,hg⟩ := mul_action.exists_smul_eq H x y,
  sorry
end

[Reid Barton]

For 1), is_pretransitive is a class which makes it awkward to use values of the type directly--you're intended to write---what Adam just wrote.

[Reid Barton]

For 2), hard to say without knowing where z' came from

[Reid Barton]

I guess that hgxy is about the action of H while z' is about the action of G--are these the same by definition? If so you might be able to use change to massage z' into the form you want

[Reid Barton]

or you can rewrite using docs#subgroup.smul_def

[Antoine Chambert-Loir]

Ruben Van de Velde said:

Can you paste a #mwe? Then people can start playing with the code

Here it is !

example (H: subgroup G) (T : X → subgroup G)
  (is_conj: ∀ g: G, ∀ x : X, T (g • x) = mul_aut.conj g • (T x))
  (is_generator: supr T = ⊤) : is_pretransitive H X → ∀(x:X), H ⊔ T x = ⊤   :=
  begin
    intros hHX x,
    apply le_antisymm le_top,
    rw [← is_generator],
    rw supr,
    refine Sup_le _,
    intros K hK, obtain ⟨y, hKy⟩:= hK, rw ← hKy,
    let z := hHX.exists_smul_eq,
    obtain ⟨g,h⟩ := z x y, rw ← h,
    let z' := is_conj (g:G) x,
    sorry,
  end

[Antoine Chambert-Loir]

Reid Barton said:

For 2), hard to say without knowing where z' came from

As you can see on the MWE, I have an hypothesis is_conj: ∀ g: G, ∀ x : X, T (g • x) = mul_aut.conj g • (T x) and I create z' by let z' := is_conj (g:G) x.

[Reid Barton]

I think using subgroup.smul_def is the way to go

[Antoine Chambert-Loir]

A new question that puzzled me for a few hours :
I need to make sense of something like this :

example (α : Type*) [A : set α] [B : set A] (p : A → Prop) (hp : ∀ (a:A), p a → a ∈ B) :
  { a : A | p a } = { b : B | p ↑b } := sorry,

What I could do is

example (α : Type*) [A : set α] [B : set A] (p : A → Prop) (hp : ∀ (a:A), p a → a ∈ B) :
  { a : A | p a } ⊆ B :=
begin
  intros a ha, rw set.mem_set_of_eq at ha, exact hp a ha,
end

but I am stuck of ideas to help me pass from the elementary second example to something that looks like the first one.

Actually, this comes from a more complicated context, group A, B : subgroup A, and ultimately, I will need to apply subgroup.closure to both sets to identify subgroup.closure { a : A | p a } with subgroup.closure { b : B | p ↑b }.

[Yaël Dillies]

This looks like you got lost in subtyping hell. Can you give the original problem instead?

[Anne Baanen]

Can the first example even be proved? The structure of the two types are different: you have (x : { b : B | p b }).1.1.1 : α but (x : { b : A | p b }).1.1 : α.

[Antoine Chambert-Loir]

Yaël Dillies said:

This looks like you got lost in subtyping hell. Can you give the original problem instead?

Sure. I want to prove that the alternating group is simple, and to start with, that it is perfect (commutator (alternating_group α) = ⊤).
I have already proved :

lemma three_cycle_is_commutator -- {α : Type*} [decidable_eq α] [fintype α]
  [h5: 5 ≤ fintype.card α] (g : alternating_group α) :
   is_three_cycle (g:perm α) → g ∈ commutator (alternating_group α) :=
begin
  intro hg,
    -- g^2 est conjugué de g : g^2 = h g h⁻¹ , donc hg = [h,g]
  let hg2 := hg.is_three_cycle_sq, -- g^2 is a 3-cycle
  rw ← subgroup.coe_mul _ g g at hg2,
  obtain ⟨h, hh⟩ := alternating_group.is_three_cycle_is_conj h5 hg hg2,
  -- g^2 is conjugate to g ;  hh :  g^2 * h = h * g
  suffices : g = h * g * h⁻¹ * g⁻¹ ,
  { apply subgroup.closure_le_normal_closure ,
    apply subgroup.subset_closure,
    rw set.mem_set_of_eq,
    exact ⟨h, g, this.symm⟩},
  exact calc g = (g * g * ↑h) * (↑h)⁻¹ * g ⁻¹ : by simp
    ... = (↑h * g) * (↑h)⁻¹  * g⁻¹  : by rw hh.symm
    ... = ↑h * g * (↑h)⁻¹ * g⁻¹ : by simp,
end

and I want to combine this with
alternating_group.closure_three_cycles_eq_alternating : closure {σ : perm α | is_three_cycle σ} = alternating_group α
(which is in alternating.lean) to get my result.

[Antoine Chambert-Loir]

Anne Baanen said:

Can the first example even be proved? The structure of the two types are different: you have (x : { b : B | p b }).1.1.1 : α but (x : { b : A | p b }).1.1 : α.

No, the types are different, but I need somehow to tell Lean that the two sets are equal, so that they will generate the same stuff afterwards…

[Johan Commelin]

This typechecks:

example (α : Type*) [A : set α] [B : set A] (p : A → Prop) (hp : ∀ (a:A), p a → a ∈ B) :
  { a : A | p a } = subtype.val '' { b : B | p ↑b } := sorry

[Anne Baanen]

Right, like @Johan Commelin suggested, we need a map to translate closure_three_cycles_eq_alternating, a statement on subgroups of perm α to a statement on subgroups of alternating_group α like your goal and three_cycle_is_commutator.

[Johan Commelin]

example (α : Type*) [A : set α] [B : set A] (p : A → Prop) (hp : ∀ (a:A), p a → a ∈ B) :
  { a : A | p a } = subtype.val '' { b : B | p ↑b } :=
begin
  ext ⟨a, ha⟩,
  simp only [set.mem_image, set_coe.exists, exists_and_distrib_right, subtype.mk_eq_mk,
    exists_eq_right, subtype.exists, set.mem_set_of_eq, subtype.coe_mk, subtype.val_eq_coe],
  split,
  { intro hpa,
    refine ⟨hp _ hpa, hpa⟩, },
  { rintro ⟨H1, H2⟩, exact H2 }
end

[Anne Baanen]

So what we're actually after is the dual form, subtype.val '⁻¹ {a : A | p a} = {b : B | p B}. Or in group-theoretic language comap (alternating_group α).subtype (closure {σ : perm α | is_three_cycle σ}) = \top.

[Johan Commelin]

Every time I see .subtype I think it's a pretty horrible name for the inclusion map.

[Johan Commelin]

I'm confused, isn't comap H.subtype H' = ⊤ simply saying that H' contains H?

[Johan Commelin]

Wouldn't it be better to write H ≤ H' in that case?

[Anne Baanen]

Indeed, that would be the next step towards proving the result :)

[Anne Baanen]

At least, I'm thinking of a proof of the lines

calc commutator (alternating_group α)
    = closure (conjugates_of_set _) : rfl
... = comap (alternating_group α).subtype (closure {σ : perm α | is_three_cycle σ}) : sorry
... = ⊤ : comap_subtype_eq_top sorry

(with comap_subtype_eq_top exactly what you mentioned)

[Anne Baanen]

(Some of these =es can equivalently be replaced ≤s of course.)

[Eric Wieser]

Johan Commelin said:

Every time I see .subtype I think it's a pretty horrible name for the inclusion map.

Note that for subalgebra it's called docs#subalgebra.val instead

[Johan Commelin]

Which makes sense, I guess. Although I think .incl is even more descriptive.

[Eric Wieser]

I think we use that name elsewhere for the inclusion map between two subobjects p1 ≤ p2

[Eric Wieser]

docs#submonoid.inclusion?

[Johan Commelin]

Right, we want both

[Eric Wieser]

I suppose incl and incl_of_le would be reasonable names

[Eric Wieser]

Although you could maybe argue that subtype.val should be renamed to subtype.incl too...

[Johan Commelin]

The difference is that x.val is dot-notation on a term of a subtype, whereas H.incl is dot-notation on a subgroup (or whatever).
Both are also function-like gadgets. But subtype.val doesn't involve a coe_to_sort, whereas H.incl does.
Maybe set.incl should exist.

[Antoine Chambert-Loir]

Your discussion lost me! I'm trying to understand what subtype.val does… Is it the inclusion map from a B (viewed as a subtype of A) to A?

[Antoine Chambert-Loir]

Thanks ! Now, to go back to my context, where I have group A and B: subgroup A, it seems that what I need to compare a given subgroup of Bwith another given subgroup of A, such as in

-- does not type - fill in ...
example (A : Type*) [group A] [B : subgroup A] (p : A → Prop) (hp : ∀(a : A), p a → a ∈ B) :
  subgroup.closure ({ a : A | p a }) = ... (subgroup.closure({ b : B | p ↑b})) := sorry

[Anne Baanen]

Indeed! And the thing you want to fill for the dots are subgroup.map B.subtype, or what I think will turn out to be easier: put subgroup.comap B.subtype on the left instead.

[Anne Baanen]

(Easier means here: "saves one rewrite step", if we did it right.)

[Kevin Buzzard]

BTW @Antoine Chambert-Loir [B : subgroup A] should probably be (B : subgroup A) or {B : subgroup A}, as subgroup is not a class so square brackets won't do anything. The point is that 99 times out 100 a type has at most one group structure on it, but certainly it's commonplace that a group can have two subgroups, so subgroup shouldn't be a class.

[Antoine Chambert-Loir]

I'm making progress… but don't you find that the following sequence of instructions is absolutely ridiculous ?

example (A : Type*) [group A] (B : subgroup A) (C : subgroup B) (a : A) (ha : a ∈ B) :
  a ∈ map B.subtype C ↔ (⟨a, ha⟩ : B) ∈ C :=
begin
  split,
  { intro h,
    obtain ⟨x, H, hH⟩ := subgroup.mem_map.mp h,
    have : a = ((⟨a, ha⟩ : B) : A),
    { apply eq.symm,
      exact set_like.coe_mk a ha, },
    rw this at hH,
    simp only [subgroup.coe_subtype, subgroup.coe_mk] at hH,
    rw this at hH,
    simp only [set_like.coe_eq_coe ] at hH,
    rw ← hH, exact H },
  { intro h,
    refine subgroup.mem_map.mpr _,
    use ⟨a, ha⟩,
    split,
    exact h,
    simp only [subgroup.coe_subtype, subgroup.coe_mk], }
end

[Kevin Buzzard]

example (A : Type*) [group A] (B : subgroup A) (C : subgroup B) (a : A) (ha : a ∈ B) :
  a ∈ map B.subtype C ↔ (⟨a, ha⟩ : B) ∈ C :=
by tidy

[Kevin Buzzard]

example (A : Type*) [group A] (B : subgroup A) (C : subgroup B) (a : A) (ha : a ∈ B) :
  a ∈ map B.subtype C ↔ (⟨a, ha⟩ : B) ∈ C :=
begin
  split,
  { rintro ⟨⟨a, ha⟩, h, rfl⟩,
    exact h },
  { rintro h,
    exact ⟨⟨a, ha⟩, h, rfl⟩ },
end

[Reid Barton]

I also found by { simp [subgroup.mem_map, set_like.exists], tauto } which may or may not be considered good style

[Eric Wieser]

Golfed further:

import group_theory.subgroup.basic
open subgroup

example (A : Type*) [group A] (B : subgroup A) (C : subgroup B) (a : A) (ha : a ∈ B) :
  a ∈ map B.subtype C ↔ (⟨a, ha⟩ : B) ∈ C :=
@function.injective.mem_set_image _ _ _ subtype.coe_injective _ ⟨a, ha⟩

[Antoine Chambert-Loir]

Y'all, you're sorcerers…

[Antoine Chambert-Loir]

Would you have a link to a description of what rintro is used, especially withrfl?

[Johan Commelin]

Hopefully tactic#rintro or tactic#rcases is helpful (edit: I guess you need to read both :smile:)

[Antoine Chambert-Loir]

Thanks ! Meanwhile, I tried entering rintroin the google search window, and guess what?…

[Adam Topaz]

Just for fun, here is an incomprehensible version of Kevin's proof ;)

example (A : Type*) [group A] (B : subgroup A) (C : subgroup B) (a : A) (ha : a ∈ B) :
  a ∈ map B.subtype C ↔ (⟨a, ha⟩ : B) ∈ C :=
⟨λ⟨⟨_,_⟩,h,rfl⟩,h,λh,⟨⟨a,_⟩,h,rfl⟩⟩

[Riccardo Brasca]

⟨a,_⟩ can be golfed to ⟨_,_⟩

[Adam Topaz]

That last rfl is doing it's job!

[Patrick Massot]

I say ⟨λ⟨⟨_,_⟩,h,rfl⟩,h,λh,⟨_,h,rfl⟩⟩

[Kevin Buzzard]

I am surprised this works -- I thought the rfl hack would not work with a lambda in term mode.

[Adam Topaz]

And now with even more underscores:
⟨λ⟨⟨_,_⟩,_,rfl⟩,‹_›,λ_,⟨⟨_,_⟩,‹_›,rfl⟩⟩

[Riccardo Brasca]

Wow!! I've never really understood what ‹_› means, but it's very nice

[Eric Rodriguez]

it's basically just a short way to write by assumption!

[Kevin Buzzard]

@Antoine Chambert-Loir here's an example of the rfl hack:

import tactic

open function

variables (X Y Z : Type) (f : X → Y) (g : Y → Z)

-- recall that surjective f := ∀ y : Y, ∃ x : X, f x = y

example (hf : surjective f) (hg : surjective g) :
  surjective (g ∘ f) :=
begin
  intro z,
  -- goal `⊢ ∃ (x : X), (g ∘ f) x = z`
  rcases hg z with ⟨y, hy⟩,
  -- `hy : g y = z`
  -- so we have a *formula* for z now, it's g(y)
  rcases hf y with ⟨x, hx⟩,
  -- and now `hx : f x = y`
  use x,
  /-
  z : Z
  y : Y
  hy : g y = z
  x : X
  hx : f x = y
  ⊢ (g ∘ f) x = z
  -/
  -- there are now several ways to finish, e.g.
  rw ← hy,
  rw ← hx,
  -- goal got closed because it's now refl and rw tries this
end

example (hf : surjective f) (hg : surjective g) :
  surjective (g ∘ f) :=
begin
  intro z,
  -- goal `⊢ ∃ (x : X), (g ∘ f) x = z`
  rcases hg z with ⟨y, rfl⟩, -- *define* z to be g(y)
  -- goal now `⊢ ∃ (a : X), (g ∘ f) a = g y`
  rcases hf y with ⟨x, rfl⟩,
  -- now there are no y's or z's in the local context, just
  /-
  x: X
  ⊢ ∃ (a : X), (g ∘ f) a = g (f x)
  -/
  use x,
  -- goal was rfl so got closed because `use` tries `triv` which tries `refl`
end

[Antoine Chambert-Loir]

Little progress, Lean knows that the alternating group is perfect… With coercion hacks showing that I didn't really understand what y'all told me yesterday. See #10253

[Johan Commelin]

@Antoine Chambert-Loir What do you think of the following approach?

-- still quite stupid, but maybe not too bad
theorem ok_lemma {G : Type*} [group G] (p : G → Prop) :
  closure {x : closure {g | p g} | p (x : G)} = ⊤ :=
begin

end

/-- If n ≥ 5, then the alternating group on n letters is perfect -/
theorem alternating_group_is_perfect (h5 : 5 ≤ fintype.card α) : commutator (alternating_group α) = ⊤ :=
begin
  suffices : closure {b : alternating_group α | (b : perm α).is_three_cycle} = ⊤,
  { rw [eq_top_iff, ← this, subgroup.closure_le],
    intros b hb,
    exact three_cycle_mem_commutator h5 hb, },
  rw [← closure_three_cycles_eq_alternating, ok_lemma],
end

[Antoine Chambert-Loir]

Let my try that, thanks!
(On the other hand, @Eric Wieser noted that the ugly_lemma matches submodule.comap_subtype_self and should be put in subgroup/basic.lean (Aside : how to refer to a file of the library or to a function so that it adds a link?)

[Eric Wieser]

you can type docs#submodule.comap_subtype_self or file#group_theory/subgroup/basic in Zulip, if that's what you mean

[Eric Wieser]

Is ok_lemma at all related to docs#subgroup.closure_closure_coe_preimage?

[Johan Commelin]

Eric Wieser said:

Is ok_lemma at all related to docs#subgroup.closure_closure_coe_preimage?

Ugh! That statement is unreadable in the docs :sad:

[Johan Commelin]

But I think it is exactly ok_lemma

[Eric Wieser]

It would be nice if we could teach doc-gen (or maybe the pretty-printer?) to show unappliedcoe with a type annotation

[Antoine Chambert-Loir]

It seems my bersion of subgroup.basic.lean is not recent enough… I tried leanproject get-cache, leanproject up, leanproject pull but nothing happens.…

[Johan Commelin]

@Antoine Chambert-Loir Please take these steps:

1. save and commit whatever you've still open
2. run git pull
3. run git merge master
4. run leanproject get-cache

[Johan Commelin]

Here's my own proof:

lemma _root_.subgroup.subtype_injective {G : Type*} [group G] (H : subgroup G) :
  function.injective H.subtype :=
subtype.val_injective

@[simp] lemma _root_.subgroup.map_top {G H : Type*} [group G] [group H] (f : G →* H) :
  subgroup.map f ⊤ = f.range :=
by { ext, simp only [iff_self, mem_map, monoid_hom.mem_range, exists_true_left],
  split, { rintro ⟨g, -, hg⟩, exact ⟨g, hg⟩ }, { rintro ⟨g, hg⟩, exact ⟨g, mem_top _, hg⟩ } }

@[simp] lemma _root_.subgroup.map_closure
  {G H : Type*} [group G] [group H] (f : G →* H) (s : set G) :
  subgroup.map f (closure s) = closure (f '' s) :=
begin
  ext h, rw [mem_map], split,
  { rintro ⟨g, hg, rfl⟩,
    refine closure_induction hg _ _ _ _,
    { intros h hh, exact subset_closure (set.mem_image_of_mem _ hh) },
    { rw f.map_one, exact one_mem _ },
    { intros h₁ h₂ hh₁ hh₂, rw f.map_mul, exact mul_mem _ hh₁ hh₂ },
    { intros h hh, rw f.map_inv, exact inv_mem _ hh } },
  { intro hh,
    refine closure_induction hh _ _ _ _,
    { rintro _ ⟨g, hg, rfl⟩, exact ⟨g, subset_closure hg, rfl⟩ },
    { exact ⟨1, one_mem _, f.map_one⟩ },
    { rintro _ _ ⟨g₁, h₁, rfl⟩ ⟨g₂, h₂, rfl⟩, exact ⟨g₁ * g₂, mul_mem _ h₁ h₂, f.map_mul _ _⟩ },
    { rintro _ ⟨g, hg, rfl⟩, exact ⟨g⁻¹, inv_mem _ hg, f.map_inv _⟩ } }
end

lemma _root_.set.coe_image_subtype_coe {α : Type*} (p : α → Prop) (s : set α)
  (h : ∀ x ∈ s, p x) :
  coe '' {x : subtype p | (x : α) ∈ s} = s :=
begin
  ext a, simp only [exists_prop, set.mem_image, subtype.exists, set.mem_set_of_eq, subtype.coe_mk],
  split, { rintro ⟨_, h1, h2, rfl⟩, exact h2 }, { intro ha, exact ⟨_, h _ ha, ha, rfl⟩ }
end

theorem ok_lemma {G : Type*} [group G] (s : set G) :
  closure {x : closure s | (x : G) ∈ s} = ⊤ :=
begin
  apply map_injective (subgroup.subtype_injective _),
  simp only [subgroup.map_closure, subgroup.map_closure, subgroup.map_top, subtype_range,
    subgroup.coe_subtype],
  congr' 1, erw [set.coe_image_subtype_coe], intros g hg, exact subset_closure hg
end

[Johan Commelin]

Looks like there's a bunch of missing lemmas. (At least I couldn't find them.)

[Eric Wieser]

subgroup.map_top is docs#monoid_hom.range_eq_map

[Eric Wieser]

subgroup.map_closure might be docs#subgroup.closure_image

[Antoine Chambert-Loir]

This works nicely, without any additional lemma !

/-- If n ≥ 5, then the alternating group on n letters is perfect -/
theorem alternating_group_is_perfect (h5 : 5 ≤ fintype.card α) : commutator (alternating_group α) = ⊤ :=
begin
  suffices : closure {b : alternating_group α | (b : perm α).is_three_cycle} = ⊤,
  { rw [eq_top_iff, ← this, subgroup.closure_le],
    intros b hb,
    exact three_cycle_mem_commutator h5 hb, },
  rw ← closure_three_cycles_eq_alternating,
  apply subgroup.closure_closure_coe_preimage ,
end

[Antoine Chambert-Loir]

Johan Commelin said:

Antoine Chambert-Loir Please take these steps:

1. save and commit whatever you've still open
2. run git pull
3. run git merge master
4. run leanproject get-cache

What is the difference with leanproject rebase, which ultimately worked?
(I had done a git stash to preserve my modifications, and a git stash pop afterwards!)

[Johan Commelin]

Aah, I didn't yet know about leanproject rebase. But it does almost the same thing under the hood.

[Antoine Chambert-Loir]

In fact, I'm not sure, I had an ugly git merge to do, but the new PR is done !

[Antoine Chambert-Loir]

Is it reasonable that I merge 232 commits into master ?
It seems I should rather revert my previous commit…

[Johan Commelin]

Yeah, that doesn't sound good.

[Johan Commelin]

The merge should rather go in the other direction

[Antoine Chambert-Loir]

This is what I think too.
I tried to do a revert, but that didn't change anything.

[Julian Berman]

(I think GitHub diff is just confused possibly, looking at and merging the branch locally it looks fine to me)

[Ruben Van de Velde]

What's your branch called?

[Eric Wieser]

It sounds like you made this classic mistake:

• git rebase
• git push, which errors saying that upstream has diverged
• git pull (the mistake)

After a rebase, you have to git push -f, not git pull

[Antoine Chambert-Loir]

So now, what should I do ?
I have tried to revert to the earlier stuff (and I have a copy of the files in their correct versions).

[Eric Wieser]

What do you mean by "revert"?

[Eric Wieser]

do you mean git revert or git reset?

[Eric Wieser]

revert is not "undo the git action I just did", it's "create a new commit that restores the files to how they were before the action I just did, on top of that action"

[Antoine Chambert-Loir]

I meant revert.…

[Eric Wieser]

git reset --hard THE_BAD_MERGE_COMMIT^ should get you back to where you were before the merge (and discard your local changes)

[Eric Wieser]

You might want to stash before that

[Kevin Buzzard]

why not just make the PR and see what happens before doing anything drastic?

[Julian Berman]

bors squashes commits though no Eric? So yeah there's a bunch of noise there but technically it should be fine no? I think you can probably get the diff un-confused even by just pushing an empty commit, or if not just opening a new PR?

[Ruben Van de Velde]

I would generally not suggest reset --hard to someone who doesn't know what that does :)

[Eric Wieser]

Kevin Buzzard said:

why not just make the PR and see what happens before doing anything drastic?

The best time to unbork git history is immediatey after you bork it

[Eric Wieser]

Otherwise you build actual work on top of it and then you're in trouble

[Antoine Chambert-Loir]

Kevin Buzzard said:

why not just make the PR and see what happens before doing anything drastic?

Nothing is really drastic, I have copies of the two files which I have modified.

[Kevin Buzzard]

then why not just make a new branch off master and copy-paste the files in :-)

[Kevin Buzzard]

that's what I usually do ;-)

[Eric Wieser]

There's no need to use a new branch; just git reset --hard origin/master and paste the files in

[Eric Wieser]

That way you can reuse the existing PR

[Eric Wieser]

Eric Wieser said:

git reset --hard THE_BAD_MERGE_COMMIT^ should get you back to where you were before the merge (and discard your local changes)

I retract this comment, it looks like you added extra commits after you made the offending merge in e5552fd2add5b8c1b157345c525484617b36d1a2, so the cleanup is much harder.

[Antoine Chambert-Loir]

All the commits that came afterwards were inoccuous.

[Eric Wieser]

Then probably the quickest recovery is:

git reset --hard d1ca2d4c03cff5087afa52545b2f35bfd7449a0b

# paste back over your files and check if anything changed that you weren't expecting, and commit them

git push --force

[Eric Wieser]

Perhaps leanproject rebase should have some heavy warnings, since using it without understanding a git rebase that well gets you in this trap.