awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
x : R
⊢ Eq (α := R) (Δ_[1] (fun (r : R) ↦ r ^ (n + 1)) x)
    ((∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i) x)

Tactic:
simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]

Premises used: fwdDiff, add_pow, mul_comm, nsmul_eq_mul, Finset.sum_range_succ
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)

Tactic:
have : (Δ_[1] fun (r : R) ↦ r ^ (n + 1)) =
      ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
succ :
  ∑ x ∈ range n, HSMul.hSMul (β := R → R) ((n + 1).choose x) (Δ_[1]^[n] fun (r : R) ↦ r ^ x) +
      HSMul.hSMul (β := R → R) ((n + 1).choose n) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) =
    (↑(n + 1)! : R → R)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ (n + 1)) (↑(n + 1)! : R → R)

Tactic:
simp_rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum, fwdDiff_iter_const_smul,
       sum_range_succ]

Premises used: fwdDiff_iter_finsetSum, Function.iterate_succ_apply, Finset.sum_range_succ, fwdDiff_iter_const_smul
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range n
⊢ i < n

Tactic:
have := mem_range.1 hi
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this_1 :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range n
this : i < n
⊢ i < n

Tactic:
lia
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range n
rw : HMul.hMul (α := R → R) (↑((n + 1).choose i) : R → R) 0 = 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := R → R) 0 0
⊢ HMul.hMul (α := R → R) (↑((n + 1).choose i) : R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ i) = 0

Tactic:
rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]

Premises used: fwdDiff_iter_pow_eq_zero_of_lt, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
⊢ ∑ x ∈ range n, HSMul.hSMul (β := R → R) ((n + 1).choose x) (Δ_[1]^[n] fun (r : R) ↦ r ^ x) +
      HSMul.hSMul (β := R → R) ((n + 1).choose n) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) =
    (↑(n + 1)! : R → R)

Tactic:
simpa [IH, factorial_succ] using sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]

Premises used: Nat.factorial_succ, Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
zero : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[0] fun (r : R) ↦ HPow.hPow (β := ℕ) r 0) (↑0! : R → R)
succ :
  ∀ (n : ℕ) (IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)),
    Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ (n + 1)) (↑(n + 1)! : R → R)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)

Tactic:
induction n with
  | zero => aesop
  | succ n IH =>
    have : (Δ_[1] fun (r : R) ↦ r ^ (n + 1)) =
      ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
    simp_rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum, fwdDiff_iter_const_smul,
       sum_range_succ]
    simpa [IH, factorial_succ] using sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]

Premises used: Nat.factorial_succ, Finset.sum_eq_zero, fwdDiff_iter_finsetSum, Function.iterate_succ_apply, Nat.zero, Nat.succ, Finset.sum_range_succ, fwdDiff_iter_const_smul
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
simp_rw :
  (∑ x ∈ range (P.natDegree + 1), HSMul.hSMul (β := R → R) (P.coeff x) (Δ_[1]^[P.natDegree] fun (i : R) ↦ i ^ x)) x =
    HSMul.hSMul (β := R) P.leadingCoeff ((↑P.natDegree ! : R → R) x)
⊢ Δ_[1]^[P.natDegree] (fun (x : R) ↦ eval x P) x = HSMul.hSMul (β := R → R) P.leadingCoeff (↑P.natDegree ! : R → R) x

Tactic:
simp_rw [P.eval_eq_sum_range, ← sum_apply _ _ (fun i x ↦ P.coeff i * x ^ i),
    fwdDiff_iter_finsetSum, ← smul_eq_mul, ← Pi.smul_def, fwdDiff_iter_const_smul, Pi.smul_apply]

Premises used: HMul.hMul, Finset.sum_apply, Polynomial.coeff, fwdDiff_iter_finsetSum, HPow.hPow, Polynomial.eval_eq_sum_range, smul_eq_mul, Pi.smul_def, fwdDiff_iter_const_smul, Pi.smul_apply
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
rw :
  ∀ (i : ℕ) (hi : i ∈ range P.natDegree),
    HSMul.hSMul (β := R → R) (P.coeff i) (Δ_[1]^[P.natDegree] fun (i_1 : R) ↦ i_1 ^ i) x = 0
⊢ (∑ x ∈ range (P.natDegree + 1), HSMul.hSMul (β := R → R) (P.coeff x) (Δ_[1]^[P.natDegree] fun (i : R) ↦ i ^ x)) x =
    HSMul.hSMul (β := R) P.leadingCoeff ((↑P.natDegree ! : R → R) x)

Tactic:
rw [sum_apply, sum_range_succ, sum_eq_zero (fun i hi ↦ ?_), zero_add,
    fwdDiff_iter_eq_factorial, leadingCoeff, Pi.smul_apply]

Premises used: Finset.sum_eq_zero, Finset.sum_apply, Polynomial.leadingCoeff, zero_add, fwdDiff_iter_eq_factorial, Finset.sum_range_succ, Pi.smul_apply
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
rw : HSMul.hSMul (β := R → R) (P.coeff i) 0 x = 0
rw₁ : Eq.{u_3 + 1} (α := R) (0 x) 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) 0 0
⊢ HSMul.hSMul (β := R → R) (P.coeff i) (Δ_[1]^[P.natDegree] fun (i_1 : R) ↦ i_1 ^ i) x = 0

Tactic:
rw [fwdDiff_iter_pow_eq_zero_of_lt (mem_range.mp hi), smul_zero, Pi.zero_apply]

Premises used: fwdDiff_iter_pow_eq_zero_of_lt, smul_zero, Pi.zero_apply, Finset.mem_range, Iff.mp
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
n : ℕ
hP : P.natDegree < n
x : R
obtain :
  ∀ (j : ℕ) (hP : P.natDegree < P.natDegree + j + 1),
    Eq.{u_3 + 1} (α := R) (Δ_[1]^[P.natDegree + j + 1] (fun (x : R) ↦ eval x P) x : R) (0 x : R)
⊢ Eq.{u_3 + 1} (α := R) (Δ_[1]^[n] (fun (x : R) ↦ eval x P) x : R) (0 x : R)

Tactic:
obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_lt hP

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
rw :
  Eq.{u_3 + 1} (α := R)
    (Δ_[1]^[j] (Δ_[1] fun (i : R) ↦ HSMul.hSMul (β := R) P.leadingCoeff ((↑P.natDegree ! : R → R) i)) x : R) (0 x : R)
⊢ Eq.{u_3 + 1} (α := R) (Δ_[1]^[P.natDegree + j + 1] (fun (x : R) ↦ eval x P) x : R) (0 x : R)

Tactic:
rw [add_assoc, add_comm, Function.iterate_add_apply, Function.iterate_succ_apply,
    P.fwdDiff_iter_degree_eq_factorial, Pi.smul_def]

Premises used: Function.iterate_add_apply, add_assoc, add_comm, Function.iterate_succ_apply, Polynomial.fwdDiff_iter_degree_eq_factorial, Pi.smul_def
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Eq.{u_3 + 1} (α := R)
    (Δ_[1]^[j] (Δ_[1] fun (i : R) ↦ HSMul.hSMul (β := R) P.leadingCoeff ((↑P.natDegree ! : R → R) i)) x : R) (0 x : R)

Tactic:
simp [fwdDiff_iter_eq_sum_shift]

Premises used: fwdDiff_iter_eq_sum_shift
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
⊢ P.natDegree < P.natDegree + 1

Tactic:
have hP : P.natDegree < P.natDegree + 1 := Nat.lt_succ_self P.natDegree
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
hP : P.natDegree < P.natDegree + 1
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[P.natDegree + 1] fun (x : R) ↦ eval x P) 0

Tactic:
Polynomial.fwdDiff_iter_eq_zero_of_degree_lt hP

Premises used: Polynomial.fwdDiff_iter_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
hP : P.natDegree < P.natDegree + 1
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[P.natDegree + 1] fun (x : R) ↦ eval x P) 0

Tactic:
exact Polynomial.fwdDiff_iter_eq_zero_of_degree_lt hP

Premises used: Polynomial.fwdDiff_iter_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
P : ℕ → R
simp_rw : Eq.{u_3 + 1} (α := R → R) (∑ c ∈ range n, HSMul.hSMul (β := R → R) (P c) (Δ_[1]^[n] fun (i : R) ↦ i ^ c)) 0
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ ∑ k ∈ range n, P k * r ^ k) 0

Tactic:
simp_rw [← sum_apply _ _ (fun i x ↦ P i * x ^ i), fwdDiff_iter_finsetSum, sum_fn, ← smul_eq_mul,
    ← Pi.smul_def, fwdDiff_iter_const_smul, ← sum_fn]

Premises used: HMul.hMul, Finset.sum_apply, fwdDiff_iter_finsetSum, HPow.hPow, Finset.sum_fn, smul_eq_mul, Pi.smul_def, fwdDiff_iter_const_smul
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
P : ℕ → R
⊢ Eq.{u_3 + 1} (α := R → R) (∑ c ∈ range n, HSMul.hSMul (β := R → R) (P c) (Δ_[1]^[n] fun (i : R) ↦ i ^ c)) 0

Tactic:
sum_eq_zero fun i hi ↦ smul_eq_zero_of_right _ <| fwdDiff_iter_pow_eq_zero_of_lt
    <| mem_range.mp hi

Premises used: fwdDiff_iter_pow_eq_zero_of_lt, Finset.sum_eq_zero, Finset.mem_range, Iff.mp, smul_eq_zero_of_right
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
P : ℕ → R
⊢ Eq.{u_3 + 1} (α := R → R) (∑ c ∈ range n, HSMul.hSMul (β := R → R) (P c) (Δ_[1]^[n] fun (i : R) ↦ i ^ c)) 0

Tactic:
exact sum_eq_zero fun i hi ↦ smul_eq_zero_of_right _ <| fwdDiff_iter_pow_eq_zero_of_lt
    <| mem_range.mp hi

Premises used: Finset.sum_eq_zero, smul_eq_zero_of_right
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H
x y : G × H
⊢ Membership.mem (γ := Set (G × H)) {x : G × H | (f : (a : G) → H) x.1 = x.2} x →
    Membership.mem (γ := Set (G × H)) {x : G × H | (f : (a : G) → H) x.1 = x.2} y →
      Membership.mem (γ := Set (G × H)) {x : G × H | (f : (a : G) → H) x.1 = x.2} (x * y)

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
inst_1 : Monoid H
f : G →* H
x : G × H
⊢ x ∈ f.mgraph ↔ (f : (a : G) → H) x.1 = x.2

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
inst_1 : Monoid H
f : G →* H
⊢ f.mgraph = mrange (MonoidHom.prod (id G) f)

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
obtain :
  ∀ (f' : H → I) (hf' : Set.range (ι := G) (⇑f : (a : G) → H × I) = graphOn f' univ),
    ∃ (f' : H →* I), mrange f = f'.mgraph
⊢ ∃ (f' : H →* I), mrange f = f'.mgraph

Tactic:
obtain ⟨f', hf'⟩ := exists_range_eq_graphOn_univ hf₁ hf

Premises used: Set.exists_range_eq_graphOn_univ
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : Set.range (ι := G) (⇑f : (a : G) → H × I) = graphOn f' univ
⊢ ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b

Tactic:
simp only [Set.ext_iff, Set.mem_range, mem_graphOn, mem_univ, true_and, Prod.forall] at hf'

Premises used: Set.mem_range, Set.mem_graphOn, Set.mem_univ, Prod.forall, Set.ext_iff, true_and
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
simp_rw :
  ∀ (x x_1 : G),
    f'
        (HMul.hMul (α := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x)
          (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x_1)) =
      f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x) *
        f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x_1)
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y

Tactic:
simp_rw [hf₁.forall]

Premises used: Function.Surjective.forall
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
g₁ g₂ : G
⊢ (f : (a : G) → H × I) (g₁ * g₂) =
    (HMul.hMul (α := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₁)
        (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₂),
      f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₁) *
        f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₂))

Tactic:
simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]

Premises used: Prod.ext_iff, Prod.fst, Exists.intro, Iff.mp, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
g₁ g₂ : G
⊢ f'
      (HMul.hMul (α := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₁)
        (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₂)) =
    f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₁) *
      f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) g₂)

Tactic:
exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩

Premises used: HMul.hMul, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
h : Eq (α := Submonoid (H × I)) (mrange f) (mgraph { toFun := f', map_one' := ⋯, map_mul' := ⋯ })
⊢ ∃ (f' : H →* I), mrange f = f'.mgraph

Tactic:
use
  { toFun := f'
    map_one' := (hf' _ _).1 ⟨1, map_one _⟩
    map_mul' := by
      simp_rw [hf₁.forall]
      rintro g₁ g₂
      exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩ }
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
⊢ Eq (α := Submonoid (H × I)) (mrange f) (mgraph { toFun := f', map_one' := ⋯, map_mul' := ⋯ })

Tactic:
simpa [SetLike.ext_iff] using hf'

Premises used: SetLike.ext_iff
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
obtain : ∀ (e₁ : H →* I) (he₁ : mrange f = e₁.mgraph), ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph
⊢ ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph

Tactic:
obtain ⟨e₁, he₁⟩ := f.exists_mrange_eq_mgraph hf₁ fun _ _ ↦ (hf _ _).1

Premises used: Iff.mp, MonoidHom.exists_mrange_eq_mgraph
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I)
    (Function.comp (β := I × H) Prod.fst (⇑(comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) : (a : G) → I × H))

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ ∀ (g₁ g₂ : G),
    Eq.{u_3 + 1} (α := I) ((comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f : (a : G) → I × H) g₁).1
        ((comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f : (a : G) → I × H) g₂).1 →
      Eq.{u_2 + 1} (α := H) ((comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f : (a : G) → I × H) g₁).2
        ((comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f : (a : G) → I × H) g₂).2

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
obtain :
  ∀ (e₂ : I →* H) (he₂ : mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) = e₂.mgraph),
    ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph
⊢ ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph

Tactic:
obtain ⟨e₂, he₂⟩ := (MulEquiv.prodComm.toMonoidHom.comp f).exists_mrange_eq_mgraph (by simpa) <|
    by simp [hf]

Premises used: MonoidHom.exists_mrange_eq_mgraph
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) = e₂.mgraph
h : H
i : I
rw :
  ∀ (he₁ : ∀ (x : H × I), Membership.mem (γ := Submonoid (H × I)) (mrange f) x ↔ x ∈ e₁.mgraph) (e₂ : I →* H)
    (he₂ :
      ∀ (x : I × H),
        Membership.mem (γ := Submonoid (I × H))
            (mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f)) x ↔
          x ∈ e₂.mgraph)
    (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
⊢ (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h

Tactic:
rw [SetLike.ext_iff] at he₁ he₂

Premises used: SetLike.ext_iff
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : ∀ (x : H × I), Membership.mem (γ := Submonoid (H × I)) (mrange f) x ↔ x ∈ e₁.mgraph
e₂ : I →* H
he₂ :
  ∀ (x : I × H),
    Membership.mem (γ := Submonoid (I × H)) (mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f))
        x ↔
      x ∈ e₂.mgraph
h : H
i : I
⊢ (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h

Tactic:
aesop (add simp [Prod.swap_eq_iff_eq_swap])

Premises used: Prod.swap_eq_iff_eq_swap