awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
⊢ ∃ (y_1 : M),
    Eq (α := M₂ × M₃) (((f : (a : M) → M₂) y_1, (g : (a : M) → M₃) y_1) : M₂ × M₃)
      (((f : (a : M) → M₂) x, (g : (a : M) → M₃) y) : M₂ × M₃)
have simp : ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
Tactic: simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
⊢ ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
have this : y - x ∈ f.ker ⊔ g.ker
Tactic: have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
⊢ ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
have rcases : ∀ (x' : M) (hx' : x' ∈ f.ker) (y' : M) (hy' : y' ∈ g.ker) (H : x' + y' = y - x),
  ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
Tactic: rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
have refine_1 : x' + x - x ∈ f.ker
Tactic: refine ⟨x' + x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
refine_1 : x' + x - x ∈ f.ker
⊢ ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
have refine_2 : Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) (x' + x) : M₃) ((g : (a : M) → M₃) y : M₃)
Tactic: refine ⟨x' + x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a b : M × M₂
ha : a.2 = (f : (a : M) → M₂) a.1
hb : b.2 = (f : (a : M) → M₂) b.1
⊢ Membership.mem (γ := Set (M × M₂)) {p : M × M₂ | p.2 = (f : (a : M) → M₂) p.1} (a + b)
have change : a.2 + b.2 = (f : (a : M) → M₂) (a.1 + b.1)
Tactic: change _ + _ = f (_ + _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a b : M × M₂
ha : a.2 = (f : (a : M) → M₂) a.1
hb : b.2 = (f : (a : M) → M₂) b.1
⊢ a.2 + b.2 = (f : (a : M) → M₂) (a.1 + b.1)
have rw : a.2 + b.2 = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
Tactic: rw [map_add, ha, hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a b : M × M₂
ha : a.2 = (f : (a : M) → M₂) a.1
hb : b.2 = (f : (a : M) → M₂) b.1
rw : a.2 + b.2 = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
⊢ a.2 + b.2 = (f : (a : M) → M₂) (a.1 + b.1)
have rw₁ : HAdd.hAdd (α := M₂) ((f : (a : M) → M₂) a.1 : M₂) b.2 =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
Tactic: rw [map_add, ha, hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a b : M × M₂
ha : a.2 = (f : (a : M) → M₂) a.1
hb : b.2 = (f : (a : M) → M₂) b.1
rw : a.2 + b.2 = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
rw₁ :
  HAdd.hAdd (α := M₂) ((f : (a : M) → M₂) a.1 : M₂) b.2 =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
⊢ a.2 + b.2 = (f : (a : M) → M₂) (a.1 + b.1)
have rw₂ : HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
Tactic: rw [map_add, ha, hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
c : R
x : M × M₂
hx : x.2 = (f : (a : M) → M₂) x.1
⊢ Membership.mem (γ := Set (M × M₂)) {p : M × M₂ | p.2 = (f : (a : M) → M₂) p.1} (c • x)
have change : c • x.2 = (f : (a : M) → M₂) (c • x.1)
Tactic: change _ • _ = f (_ • _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
c : R
x : M × M₂
hx : x.2 = (f : (a : M) → M₂) x.1
⊢ c • x.2 = (f : (a : M) → M₂) (c • x.1)
have rw : c • x.2 = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x.1 : M₂)
Tactic: rw [map_smul, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
c : R
x : M × M₂
hx : x.2 = (f : (a : M) → M₂) x.1
rw : c • x.2 = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x.1 : M₂)
⊢ c • x.2 = (f : (a : M) → M₂) (c • x.1)
have rw₁ : HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x.1 : M₂) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x.1 : M₂)
Tactic: rw [map_smul, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommGroup M₃
inst_2 : AddCommGroup M₄
inst_3 : Module R M₃
inst_4 : Module R M₄
g : M₃ →ₗ[R] M₄
⊢ g.graph = ((-g).coprod id).ker
have h : ∀ (x : M₃ × M₄), x ∈ g.graph ↔ x ∈ ((-g).coprod id).ker
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommGroup M₃
inst_2 : AddCommGroup M₄
inst_3 : Module R M₃
inst_4 : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x ∈ g.graph ↔ x ∈ ((-g).coprod id).ker
have h : x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (α := M₄) (-(g : (a : M₃) → M₄) x.1 : M₄) x.2 = 0
Tactic: change _ = _ ↔ -g x.1 + x.2 = _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommGroup M₃
inst_2 : AddCommGroup M₄
inst_3 : Module R M₃
inst_4 : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (α := M₄) (-(g : (a : M₃) → M₄) x.1 : M₄) x.2 = 0
have h : x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (β := M₄) x.2 (-(g : (a : M₃) → M₄) x.1 : M₄) = 0
Tactic: rw [add_comm, add_neg_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommGroup M₃
inst_2 : AddCommGroup M₄
inst_3 : Module R M₃
inst_4 : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
h : x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (β := M₄) x.2 (-(g : (a : M₃) → M₄) x.1 : M₄) = 0
⊢ x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (α := M₄) (-(g : (a : M₃) → M₄) x.1 : M₄) x.2 = 0
have h₁ : x.2 = (g : (a : M₃) → M₄) x.1 ↔ x.2 = (g : (a : M₃) → M₄) x.1
Tactic: rw [add_comm, add_neg_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
⊢ f.graph = (prod id f).range
have h : ∀ (x : M × M₂), x ∈ f.graph ↔ x ∈ (prod id f).range
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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 →ₗ[S] I), f.range = f'.graph
have obtain : ∀ (f' : H →+ I) (hf' : AddMonoidHom.mrange (F := G →+ H × I) (↑f : G →+ H × I) = f'.mgraph),
  ∃ (f' : H →ₗ[S] I), f.range = f'.graph
Tactic: obtain ⟨f', hf'⟩ :=
    AddMonoidHom.exists_mrange_eq_mgraph (G := G) (H := H) (I := I) (f := f) hf₁ hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
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' : AddMonoidHom.mrange (F := G →+ H × I) (↑f : G →+ H × I) = f'.mgraph
⊢ ∃ (f' : H →ₗ[S] I), f.range = f'.graph
have hf'₁ : ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2
Tactic: simp only [SetLike.ext_iff, AddMonoidHom.mem_mrange, AddMonoidHom.coe_coe,
    AddMonoidHom.mem_mgraph] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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' : ZeroHom H I).toFun (s • h) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) ((↑f' : ZeroHom H I).toFun h)
have simp : (f' : (a : H) → I) (s • h) = HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I)
Tactic: simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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)
have refine : ∃ (x : G), (f : (a : G) → H × I) x = (s • h, HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I))
Tactic: refine (hf' (s • h, _)).mp ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
⊢ ∃ (x : G), (f : (a : G) → H × I) x = (s • h, HSMul.hSMul (β := I) s ((f' : (a : H) → I) h : I))
have rw : HSMul.hSMul (β := H × I) s ((h, (f' : (a : H) → I) h) : H × I) ∈ f.range
Tactic: rw [← Prod.smul_mk, ← LinearMap.mem_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
⊢ HSMul.hSMul (β := H × I) s ((h, (f' : (a : H) → I) h) : H × I) ∈ f.range
have h₁ : Membership.mem (α := H × I) f.range ((h, (f' : (a : H) → I) h) : H × I)
Tactic: apply Submodule.smul_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
⊢ Membership.mem (α := H × I) f.range ((h, (f' : (a : H) → I) h) : H × I)
have h₁ : ∃ (y : G), Eq (α := H × I) ((f : (a : G) → H × I) y : H × I) ((h, (f' : (a : H) → I) h) : H × I)
Tactic: rw [LinearMap.mem_range, hf']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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)
⊢ Membership.mem (α := H × I) f.range ((h, (f' : (a : H) → I) h) : H × I)
have 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)
Tactic: rw [LinearMap.mem_range, hf']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
⊢ ∃ (f' : H →ₗ[S] I), f.range = f'.graph
have h : f.range = graph { toFun := (↑f' : ZeroHom H I).toFun, map_add' := sorry, map_smul' := sorry }
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'] }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
⊢ f.range = graph { toFun := (↑f' : ZeroHom H I).toFun, map_add' := ⋯, map_smul' := ⋯ }
have h : ∀ (x : H × I),
  x ∈ f.range ↔
    Membership.mem (γ := Submodule S (H × I))
      (graph { toFun := (↑f' : ZeroHom H I).toFun, map_add' := sorry, map_smul' := sorry }) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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), f.range = (↑e : H →ₗ[S] I).graph
have obtain : ∀ (e₁ : H →ₗ[S] I) (he₁ : f.range = e₁.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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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 : H ≃ₗ[S] I), f.range = (↑e : H →ₗ[S] I).graph
have 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
Tactic: obtain ⟨e₂, he₂⟩ := ((LinearEquiv.prodComm _ _ _).toLinearMap.comp f).exists_range_eq_graph
    (by simpa) <| by simp [hf]