awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.sup' hs fun (x : ι) ↦ f x a) a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a
have simp : ∀ (ha : Ne.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1), ∃ i ∈ s, f i a ≠ 1
Tactic: simp only [mem_mulSupport, SetLike.mem_coe, Set.mem_iUnion, exists_prop] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Ne.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1
⊢ ∃ i ∈ s, f i a ≠ 1
have contrapose! : ∀ (ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1), Eq.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
⊢ Set.Finite.{u_1} (α := α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.inf' hs fun (x : ι) ↦ f x a)
have refine : ∀ (a : α)
  (ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.inf' hs fun (x : ι) ↦ f x a) a),
  Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a
Tactic: refine (s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.inf' hs fun (x : ι) ↦ f x a) a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a
have simp : ∀ (ha : Ne.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1), ∃ i ∈ s, f i a ≠ 1
Tactic: simp only [mem_mulSupport, SetLike.mem_coe, Set.mem_iUnion, exists_prop] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Ne.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1
⊢ ∃ i ∈ s, f i a ≠ 1
have contrapose! : ∀ (ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1), Eq.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport (f ∘ g)
have refine : Set.MapsTo g (mulSupport (f ∘ g)) (mulSupport f)
Tactic: refine Set.Finite.of_injOn ?_ (Set.injOn_of_injective hg) hf
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
inst_1 : One β
hfg : HasFiniteMulSupport (f ∘ g)
h : f 1 = 1
hf : Injective f
⊢ HasFiniteMulSupport g
have refine : ∀ (x : α) (ha : x ∈ mulSupport g) (H : (f ∘ g) x = 1), g x = 1
Tactic: refine Set.Finite.subset hfg fun _ ha ↦ Set.mem_setOf.mpr fun H ↦ Set.mem_setOf.mp ha ?_
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_4} (M := M) fun (a : α) ↦ f a ^ g a) a
⊢ a ∈ support g
have contrapose! : ∀ (ha : a ∉ support g), a ∉ mulSupport.{u_1, u_4} (M := M) fun (a : α) ↦ f a ^ g a
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (M := N₂) (N := N₃) (P := N₄) (⇑g₂ : (a : N₂) → N₃) (⇑g₃ : (a : N₃) → N₄)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₃ : Function.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
have obtain : ∀ (y : M₃) (hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) y : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)),
  ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
Tactic: obtain ⟨y, hy⟩ := hi₃ (g₂ x)
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (M := N₂) (N := N₃) (P := N₄) (⇑g₂ : (a : N₂) → N₃) (⇑g₃ : (a : N₃) → N₄)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₃ : Function.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
y : M₃
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) y : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
have obtain : ∀ (a : M₂)
  (hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)),
  ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
Tactic: obtain ⟨a, rfl⟩ : y ∈ Set.range f₂ := (hf₂ _).mp <| by
    simpa [hy, hg₂.apply_apply_eq_one, map_eq_one_iff _ hi₄] using (DFunLike.congr_fun hc₃ y).symm
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (M := N₂) (N := N₃) (P := N₄) (⇑g₂ : (a : N₂) → N₃) (⇑g₃ : (a : N₃) → N₄)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₃ : Function.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
have obtain : ∀ (b : N₁) (hb : (g₁ : (a : N₁) → N₂) b = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)),
  ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
Tactic: obtain ⟨b, hb⟩ : x / i₂ a ∈ Set.range g₁ := (hg₁ _).mp <| by
    simp [← hy, show g₂ (i₂ a) = i₃ (f₂ a) by simpa using DFunLike.congr_fun hc₂ a]
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (M := N₂) (N := N₃) (P := N₄) (⇑g₂ : (a : N₂) → N₃) (⇑g₃ : (a : N₃) → N₄)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₃ : Function.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
b : N₁
hb : (g₁ : (a : N₁) → N₂) b = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
have obtain : ∀ (o : M₁)
  (hb : (g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) o : N₁) = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)),
  ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
Tactic: obtain ⟨o, rfl⟩ := hi₁ b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (M := N₂) (N := N₃) (P := N₄) (⇑g₂ : (a : N₂) → N₃) (⇑g₃ : (a : N₃) → N₄)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₃ : Function.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
o : M₁
hb : (g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) o : N₁) = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
have h : (i₂ : (a : M₂) → N₂) (HMul.hMul (α := M₂) ((f₁ : (a : M₁) → M₂) o : M₂) a) = x
Tactic: use f₁ o * a
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group N₁
inst_4 : Group N₂
inst_5 : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₂ : Function.Surjective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₃ : Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
have refine : ∀ (y : N₁),
  Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔
    Membership.mem (γ := Set N₁) (Set.range (ι := Unit) (⇑1 : (a : Unit) → N₁)) y
Tactic: refine surjective_of_surjective_of_surjective_of_injective (1 : Unit →* M₁) f₁ f₂ (1 : Unit →* N₁)
    g₁ g₂ 1 i₁ i₂ i₃ (by simp) hc₁ hc₂ hf₁ (fun y ↦ ?_) hg₁ (fun | .unit => ⟨0, rfl⟩) hi₂ hi₃
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group N₁
inst_4 : Group N₂
inst_5 : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₂ : Function.Surjective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₃ : Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
y : N₁
⊢ Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔
    Membership.mem (γ := Set N₁) (Set.range (ι := Unit) (⇑1 : (a : Unit) → N₁)) y
have simp : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔ 1 = y
Tactic: simp only [Set.mem_range, one_apply, exists_const]
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
⊢ Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
have rw : ∀ (a : M₃), Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) (1 : N₃) → a = 1
Tactic: rw [injective_iff_map_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
m : M₃
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) m : N₃) (1 : N₃)
h : Eq.{u_9 + 1} (α := N₄) ((i₄ : (a : M₄) → N₄) ((f₃ : (a : M₃) → M₄) m : M₄) : N₄) (1 : N₄)
⊢ Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)
have rwa : ∀ (h : Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)),
  Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)
Tactic: rwa [map_eq_one_iff _ hi₄] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
m : M₃
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) m : N₃) (1 : N₃)
⊢ Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)
have suffices : Eq.{u_9 + 1} (α := N₄) ((i₄ : (a : M₄) → N₄) ((f₃ : (a : M₃) → M₄) m : M₄) : N₄) (1 : N₄)
Tactic: suffices h : i₄ (f₃ m) = 1 by rwa [map_eq_one_iff _ hi₄] at h
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
m : M₃
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) m : N₃) (1 : N₃)
⊢ m = 1
have obtain : ∀ (x : M₂) (hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)),
  Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
Tactic: obtain ⟨x, rfl⟩ := (hf₂ m).mp <| by
    suffices h : i₄ (f₃ m) = 1 by rwa [map_eq_one_iff _ hi₄] at h
    simp [← show g₃ (i₃ m) = i₄ (f₃ m) by simpa using DFunLike.congr_fun hc₃ m, hm]
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
have obtain : ∀ (y : N₁) (hy : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)),
  Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
Tactic: obtain ⟨y, hy⟩ := (hg₁ _).mp <| by
    rwa [show g₂ (i₂ x) = i₃ (f₂ x) by simpa using DFunLike.congr_fun hc₂ x]
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
y : N₁
hy : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
have obtain : ∀ (a : M₁)
  (hy : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) a : N₁) : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)),
  Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
Tactic: obtain ⟨a, rfl⟩ := hi₁ y
Cleared hypotheses: y, hy