awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
s : S
h : H
simp : (f' : (a : H) → I) (s • h) = HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I)
⊢ (↑f' : ZeroHom H I).toFun (s • h) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) ((↑f' : ZeroHom H I).toFun h)

Tactic:
simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]

Premises used: RingHom.id_apply, AddMonoidHom.toZeroHom_coe, ZeroHom.toFun_eq_coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
s : S
h : H
⊢ (f' : (a : H) → I) (s • h) = HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I)

Tactic:
(hf' (s • h, _)).mp ?_

Premises used: Prod.mk, Iff.mp, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
s : S
h : H
refine : ∃ (x : G), (f : (a : G) → H × I) x = (s • h, HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I))
⊢ (f' : (a : H) → I) (s • h) = HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I)

Tactic:
refine (hf' (s • h, _)).mp ?_

Premises used: Prod.mk, Iff.mp, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
s : S
h : H
rw : HSMul.hSMul (β := H × I) s ((h, (f' : (a : H) → I) h) : H × I) ∈ f.range
⊢ ∃ (x : G), (f : (a : G) → H × I) x = (s • h, HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I))

Tactic:
rw [← Prod.smul_mk, ← LinearMap.mem_range]

Premises used: LinearMap.mem_range, Prod.smul_mk
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
s : S
h : H
h₁ : Membership.mem (α := H × I) f.range ((h, (f' : (a : H) → I) h) : H × I)
⊢ HSMul.hSMul (β := H × I) s ((h, (f' : (a : H) → I) h) : H × I) ∈ f.range

Tactic:
apply Submodule.smul_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
s : S
h : H
h₁ : ∃ (y : G), Eq (α := H × I) ((f : (a : G) → H × I) y : H × I) ((h, (f' : (a : H) → I) h) : H × I)
h₂ h₃ :
  Eq.{u_7 + 1} (α := I) ((f' : (a : H) → I) ((h, (f' : (a : H) → I) h) : H × I).1 : I) ((h, (f' : (a : H) → I) h).2 : I)
⊢ Membership.mem (α := H × I) f.range ((h, (f' : (a : H) → I) h) : H × I)

Tactic:
rw [LinearMap.mem_range, hf']

Premises used: LinearMap.mem_range
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
h : f.range = graph { toFun := (↑f' : ZeroHom H I).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ ∃ (f' : H →ₗ[S] I), f.range = f'.graph

Tactic:
use
  { toFun := f'.toFun
    map_add' := f'.map_add'
    map_smul' := by
      intro s h
      simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]
      refine (hf' (s • h, _)).mp ?_
      rw [← Prod.smul_mk, ← LinearMap.mem_range]
      apply Submodule.smul_mem
      rw [LinearMap.mem_range, hf'] }
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
h :
  ∀ (x : H × I),
    x ∈ f.range ↔
      Membership.mem (γ := Submodule S (H × I))
        (graph { toFun := (↑f' : ZeroHom H I).toFun, map_add' := ⋯, map_smul' := ⋯ }) x
⊢ f.range = graph { toFun := (↑f' : ZeroHom H I).toFun, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
x : H × I
⊢ x ∈ f.range ↔
    Membership.mem (γ := Submodule S (H × I))
      (graph { toFun := (↑f' : ZeroHom H I).toFun, map_add' := ⋯, map_smul' := ⋯ }) x

Tactic:
simpa only [mem_range, Eq.comm, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, mem_graph_iff,
    coe_mk, AddHom.coe_mk, AddMonoidHom.coe_coe, Set.mem_range] using hf' x

Premises used: LinearMap.coe_mk, Set.mem_range, AddMonoidHom.toZeroHom_coe, AddMonoidHom.coe_coe, LinearMap.mem_range, Eq.comm, LinearMap.mem_graph_iff, AddHom.coe_mk, ZeroHom.toFun_eq_coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
S : Type u_4
H : Type u_6
I : Type u_7
inst : Semiring S
inst_1 : AddCommMonoid H
inst_2 : Module S H
inst_3 : AddCommMonoid I
inst_4 : Module S I
G : Submodule S (H × I)
hf₁ : Bijective (α := ↥G) (β := H) (comp (β := H × I) Prod.fst (⇑G.subtype : (a : ↥G) → H × I))
⊢ ∃ (f : H →ₗ[S] I), G = f.graph

Tactic:
simpa only [range_subtype] using LinearMap.exists_range_eq_graph hf₁.surjective
      (fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hf₁.injective h))

Premises used: Function.comp, Function.Bijective.injective, congr_arg, Function.Bijective.surjective, Submodule.subtype, Submodule.range_subtype, Prod.snd, DFunLike.coe, LinearMap.exists_range_eq_graph
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
obtain : ∀ (e₁ : H →ₗ[S] I) (he₁ : f.range = e₁.graph), ∃ (e : H ≃ₗ[S] I), f.range = (↑e : H →ₗ[S] I).graph
⊢ ∃ (e : H ≃ₗ[S] I), f.range = (↑e : H →ₗ[S] I).graph

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

Premises used: Iff.mp, LinearMap.exists_range_eq_graph
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
⊢ Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I)
    (Function.comp (β := I × H) Prod.fst
      (⇑((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f) : (a : G) → I × H))

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
⊢ ∀ (g₁ g₂ : G),
    Eq.{u_7 + 1} (α := I) (((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f : (a : G) → I × H) g₁).1
        (((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f : (a : G) → I × H) g₂).1 →
      Eq.{u_6 + 1} (α := H) (((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f : (a : G) → I × H) g₁).2
        (((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f : (a : G) → I × H) g₂).2

Tactic:
simp [hf]
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
obtain :
  ∀ (e₂ : I →ₗ[S] H) (he₂ : ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range = e₂.graph),
    ∃ (e : H ≃ₗ[S] I), f.range = (↑e : H →ₗ[S] I).graph
⊢ ∃ (e : H ≃ₗ[S] I), f.range = (↑e : H →ₗ[S] I).graph

Tactic:
obtain ⟨e₂, he₂⟩ := ((LinearEquiv.prodComm _ _ _).toLinearMap.comp f).exists_range_eq_graph
    (by simpa) <| by simp [hf]

Premises used: LinearMap.exists_range_eq_graph
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range = e₂.graph
h : H
i : I
⊢ ∀ (x : H × I), x ∈ f.range ↔ x.2 = (e₁ : (a : H) → I) x.1

Tactic:
simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂

Premises used: SetLike.ext_iff, LinearMap.mem_graph_iff
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range = e₂.graph
h : H
i : I
he₃ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = (e₁ : (a : H) → I) x.1
⊢ ∀ (x : I × H), x ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range ↔ x.2 = (e₂ : (a : I) → H) x.1

Tactic:
simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂

Premises used: SetLike.ext_iff, LinearMap.mem_graph_iff
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = (e₁ : (a : H) → I) x.1
he₂ :
  ∀ (x : I × H), x ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range ↔ x.2 = (e₂ : (a : I) → H) x.1
rw : (h, i) ∈ f.range ↔ (i, h) ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range
⊢ (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h

Tactic:
rw [Eq.comm, ← he₁ (h, i), Eq.comm, ← he₂ (i, h)]

Premises used: Prod.mk, Eq.comm
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = (e₁ : (a : H) → I) x.1
he₂ :
  ∀ (x : I × H), x ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range ↔ x.2 = (e₂ : (a : I) → H) x.1
⊢ (h, i) ∈ f.range ↔ (i, h) ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range

Tactic:
simp only [mem_range, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.prodComm_apply, Prod.swap_eq_iff_eq_swap, Prod.swap_prod_mk]

Premises used: Prod.swap_eq_iff_eq_swap, Prod.swap_prod_mk, LinearEquiv.prodComm_apply, LinearMap.coe_comp, LinearMap.mem_range, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range = e₂.graph
⊢ ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h

Tactic:
have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂
    rw [Eq.comm, ← he₁ (h, i), Eq.comm, ← he₂ (i, h)]
    simp only [mem_range, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.prodComm_apply, Prod.swap_eq_iff_eq_swap, Prod.swap_prod_mk]
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
h : H
rw rw₁ : Eq.{u_7 + 1} (α := I) ((e₁ : (a : H) → I) h : I) ((e₁ : (a : H) → I) h : I)
⊢ (e₂ : (a : I) → H) ((e₁ : (a : H) → I) h : I) = h

Tactic:
rw [← he₁₂]
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
i : I
rw rw₁ : Eq.{u_6 + 1} (α := H) ((e₂ : (a : I) → H) i : H) ((e₂ : (a : I) → H) i : H)
⊢ (e₁ : (a : H) → I) ((e₂ : (a : I) → H) i : H) = i

Tactic:
rw [he₁₂]