awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
⊢ RootPairing.IsIrreducible (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) ↔ IsSimple K L
have a : Nontrivial L
Tactic: nontriviality L
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
h : Nontrivial L
⊢ RootPairing.IsIrreducible (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) ↔ IsSimple K L
have hL : ¬IsLieAbelian L
Tactic: have hL : ¬ IsLieAbelian L :=
    (isLieAbelian_iff_subsingleton K (L := L)).not.mpr (not_subsingleton L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
h : Nontrivial L
hL : ¬IsLieAbelian L
⊢ RootPairing.IsIrreducible (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) ↔ IsSimple K L
have rw : IsSimpleOrder ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
  IsSimple K L
Tactic: rw [RootPairing.isIrreducible_iff_invtRootSubmodule, ← isSimple_iff_of_not_isLieAbelian K L hL,
    (lieIdealOrderIso H).isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
h : Nontrivial L
hL : ¬IsLieAbelian L
rw :
  IsSimpleOrder
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
    IsSimple K L
⊢ RootPairing.IsIrreducible (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) ↔ IsSimple K L
have rw₁ : IsSimpleOrder ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
  IsSimpleOrder.{u_2} (LieIdeal K L)
Tactic: rw [RootPairing.isIrreducible_iff_invtRootSubmodule, ← isSimple_iff_of_not_isLieAbelian K L hL,
    (lieIdealOrderIso H).isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
h : Nontrivial L
hL : ¬IsLieAbelian L
rw :
  IsSimpleOrder
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
    IsSimple K L
rw₁ :
  IsSimpleOrder
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
    IsSimpleOrder.{u_2} (LieIdeal K L)
⊢ RootPairing.IsIrreducible (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) ↔ IsSimple K L
have rw₂ : IsSimpleOrder ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
  IsSimpleOrder ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
Tactic: rw [RootPairing.isIrreducible_iff_invtRootSubmodule, ← isSimple_iff_of_not_isLieAbelian K L hL,
    (lieIdealOrderIso H).isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : R
h : a + b = 1
x : M
⊢ a • x + b • x = x
have rw : (a + b) • x = x
Tactic: rw [← add_smul, h, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : R
h : a + b = 1
x : M
rw : (a + b) • x = x
⊢ a • x + b • x = x
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = x
Tactic: rw [← add_smul, h, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : R
h : a + b = 1
x : M
rw : (a + b) • x = x
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = x
⊢ a • x + b • x = x
have rw₂ : x = x
Tactic: rw [← add_smul, h, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 2 x = x + x
have rw : HAdd.hAdd (α := R) 1 1 • x = x + x
Tactic: rw [← one_add_one_eq_two, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
rw : HAdd.hAdd (α := R) 1 1 • x = x + x
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 2 x = x + x
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = x + x
Tactic: rw [← one_add_one_eq_two, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
rw : HAdd.hAdd (α := R) 1 1 • x = x + x
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = x + x
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 2 x = x + x
have rw₂ : x + x = x + x
Tactic: rw [← one_add_one_eq_two, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
c₁ c₂ : R
x : M₂
⊢ (c₁ + c₂) • x = c₁ • x + c₂ • x
have rcases : ∀ (x : M),
  HSMul.hSMul (β := M₂) (c₁ + c₂) ((f : (a : M) → M₂) x : M₂) =
    HSMul.hSMul (β := M₂) c₁ ((f : (a : M) → M₂) x : M₂) + HSMul.hSMul (β := M₂) c₂ ((f : (a : M) → M₂) x : M₂)
Tactic: rcases hf x with ⟨x, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
x : M₂
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 x = 0
have rcases : ∀ (x : M), HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = 0
Tactic: rcases hf x with ⟨x, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
x : M
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = 0
have rw : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = (f : (a : M) → M₂) 0
Tactic: rw [← f.map_zero, ← smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
x : M
rw : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = (f : (a : M) → M₂) 0
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = 0
have rw₁ : Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x) : M₂) ((f : (a : M) → M₂) 0 : M₂)
Tactic: rw [← f.map_zero, ← smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
x : M
rw : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = (f : (a : M) → M₂) 0
rw₁ :
  Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x) : M₂)
    ((f : (a : M) → M₂) 0 : M₂)
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = 0
have rw₂ : Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) 0 : M₂) ((f : (a : M) → M₂) 0 : M₂)
Tactic: rw [← f.map_zero, ← smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
zero_eq_one : Eq.{u_1 + 1} (α := R) 0 1
⊢ x = 0
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = 0
Tactic: rw [← one_smul R x, ← zero_eq_one, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
zero_eq_one : Eq.{u_1 + 1} (α := R) 0 1
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = 0
⊢ x = 0
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x = 0
Tactic: rw [← one_smul R x, ← zero_eq_one, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
zero_eq_one : Eq.{u_1 + 1} (α := R) 0 1
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x = 0
⊢ x = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [← one_smul R x, ← zero_eq_one, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
M : Type u_3
inst : AddCommMonoid M
R : Type u_5
inst_1 : Ring R
inst_2 : Module R M
r : R
m : M
⊢ r • m + (1 - r) • m = m
have rw : (r + (1 - r)) • m = m
Tactic: rw [← add_smul, add_sub_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
M : Type u_3
inst : AddCommMonoid M
R : Type u_5
inst_1 : Ring R
inst_2 : Module R M
r : R
m : M
rw : (r + (1 - r)) • m = m
⊢ r • m + (1 - r) • m = m
have rw₁ : HSMul.hSMul.{u_5, u_3, u_3} (α := R) 1 m = m
Tactic: rw [← add_smul, add_sub_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
M : Type u_3
inst : AddCommMonoid M
R : Type u_5
inst_1 : Ring R
inst_2 : Module R M
r : R
m : M
rw : (r + (1 - r)) • m = m
rw₁ : HSMul.hSMul.{u_5, u_3, u_3} (α := R) 1 m = m
⊢ r • m + (1 - r) • m = m
have rw₂ : m = m
Tactic: rw [← add_smul, add_sub_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)
have rw : a • x + b • y = b • y + a • x
Tactic: rw [sub_add_add_cancel, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
a b : R
h : a + b = 1
rw : a • x + b • y = b • y + a • x
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)
have rw₁ : b • y + a • x = b • y + a • x
Tactic: rw [sub_add_add_cancel, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x
have rw : b • y - b • x + (a • x + b • x) = b • y - b • x + x
Tactic: rw [smul_sub, Convex.combo_self h]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
a b : R
h : a + b = 1
rw : b • y - b • x + (a • x + b • x) = b • y - b • x + x
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x
have rw₁ : b • y - b • x + x = b • y - b • x + x
Tactic: rw [smul_sub, Convex.combo_self h]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_5
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
⊢ P = Q
have smul : ∀ (x : R) (x_1 : M), SMul.smul x x_1 = SMul.smul x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
⊢ -r • x + r • x = 0
have rw : (-r + r) • x = 0
Tactic: rw [← add_smul, neg_add_cancel, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
rw : (-r + r) • x = 0
⊢ -r • x + r • x = 0
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x = 0
Tactic: rw [← add_smul, neg_add_cancel, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
rw : (-r + r) • x = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x = 0
⊢ -r • x + r • x = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [← add_smul, neg_add_cancel, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
⊢ -r • -x = r • x
have rw : -(r • -x) = r • x
Tactic: rw [neg_smul, smul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
rw : -(r • -x) = r • x
⊢ -r • -x = r • x
have rw₁ : - -(r • x) = r • x
Tactic: rw [neg_smul, smul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
rw : -(r • -x) = r • x
rw₁ : - -(r • x) = r • x
⊢ -r • -x = r • x
have rw₂ : r • x = r • x
Tactic: rw [neg_smul, smul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.DivisionRing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R) ↔ f ≠ 0
have refine : ∀ (hf : f ≠ 0) (z : R), ∃ (a : M), (f : (a : M) → R) a = z
Tactic: refine ⟨ne_zero_of_surjective, fun hf z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.DivisionRing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
⊢ ∃ (a : M), (f : (a : M) → R) a = z
have obtain : ∀ (y : M) (hy : Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)), ∃ (a : M), (f : (a : M) → R) a = z
Tactic: obtain ⟨y, hy⟩ : ∃ y, f y ≠ 0 := by simpa [Ne, LinearMap.ext_iff] using hf
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.DivisionRing (goal)
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
⊢ Membership.mem (γ := Submodule R M₁) (range (f.smulRight x)) z ↔ Membership.mem (γ := Submodule R M₁) (R ∙ x) z
have simp_rw : (∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z) ↔ ∃ (a : R), a • x = z
Tactic: simp_rw [mem_range, smulRight_apply, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.DivisionRing (goal)
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
⊢ (∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z) ↔ ∃ (a : R), a • x = z
have refine : (∃ (a : R), a • x = z) →
  ∀ (w : R) (hw : w • x = z), ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z
Tactic: refine ⟨fun ⟨w, hw⟩ ↦ ⟨f w, hw ▸ rfl⟩, fun ⟨w, hw⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.DivisionRing (goal)
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
h : ∃ (a : R), a • x = z
w : R
hw : w • x = z
⊢ ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z
have obtain : ∀ (y : M) (hw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z),
  ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z
Tactic: obtain ⟨y, rfl⟩ := hf w
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Algebra.Module.RingHom (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
M₂ : Type u_4
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
r s : R_1
x_1 : M_1
R : Type u_5
S : Type u_6
M : Type u_7
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Semiring S
inst_7 : SMul S M
f : R →+* S
hf : Surjective.{u_5 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hsmul : ∀ (c : R) (x : M), HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) c : S) x = c • x
x : M
⊢ HSMul.hSMul.{u_6, u_7, u_7} (α := S) 0 x = 0
have rw : HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) 0 : S) x = 0
Tactic: rw [← f.map_zero, hsmul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.RingHom (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
M₂ : Type u_4
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
r s : R_1
x_1 : M_1
R : Type u_5
S : Type u_6
M : Type u_7
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Semiring S
inst_7 : SMul S M
f : R →+* S
hf : Surjective.{u_5 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hsmul : ∀ (c : R) (x : M), HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) c : S) x = c • x
x : M
rw : HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) 0 : S) x = 0
⊢ HSMul.hSMul.{u_6, u_7, u_7} (α := S) 0 x = 0
have rw₁ : HSMul.hSMul.{u_5, u_7, u_7} (α := R) 0 x = 0
Tactic: rw [← f.map_zero, hsmul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.RingHom (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
M₂ : Type u_4
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
r s : R_1
x_1 : M_1
R : Type u_5
S : Type u_6
M : Type u_7
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Semiring S
inst_7 : SMul S M
f : R →+* S
hf : Surjective.{u_5 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hsmul : ∀ (c : R) (x : M), HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) c : S) x = c • x
x : M
rw : HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) 0 : S) x = 0
rw₁ : HSMul.hSMul.{u_5, u_7, u_7} (α := R) 0 x = 0
⊢ HSMul.hSMul.{u_6, u_7, u_7} (α := S) 0 x = 0
have rw₂ : Eq.{u_7 + 1} (α := M) 0 0
Tactic: rw [← f.map_zero, hsmul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ N ≤ f.ker ↔ f ∘ₛₗ N.subtype = 0
have rw : (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔
  ∀ (a : M) (b : a ∈ N),
    Eq.{u_7 + 1} (α := M₂) ((f ∘ₛₗ N.subtype : (a : ↥N) → M₂) (Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M₂)
      ((0 : (a : ↥N) → M₂) (Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M₂)
Tactic: rw [SetLike.le_def, LinearMap.ext_iff, Subtype.forall]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ f.ker ≤ (g ∘ₛₗ f).ker
have rw : f.ker ≤ comap f g.ker
Tactic: rw [ker_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ⊔ g.ker ≤ (f ∘ₗ g).ker
have refine : f.ker ≤ (f ∘ₗ g).ker
Tactic: refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ≤ (f ∘ₗ g).ker
have rw : f.ker ≤ (g ∘ₗ f).ker
Tactic: rw [← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) (0 : M₂)
⊢ m = 0
have rw : Eq (α := M) ((id : (a : M) → M) m : M) (0 : M)
Tactic: rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) (0 : M₂)
rw : Eq (α := M) ((id : (a : M) → M) m : M) (0 : M)
⊢ m = 0
have rw₁ : Eq (α := M) ((g ∘ₛₗ f : (a : M) → M) m : M) (0 : M)
Tactic: rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) (0 : M₂)
rw : Eq (α := M) ((id : (a : M) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((g ∘ₛₗ f : (a : M) → M) m : M) (0 : M)
⊢ m = 0
have rw₂ : Eq.{u_5 + 1} (α := M) ((g : (a : M₂) → M) ((f : (a : M) → M₂) m : M₂) : M) (0 : M)
Tactic: rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]