awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
h_1 : Nontrivial M
α : S
hα : (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
β : S
hβ : (⇑g : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) β (⇑f : (a : M) → M₂)
⊢ ∃ (α : Sˣ), f = α • g
have neg : ∀ (x : M) (hx : x ≠ 0), ∃ (α : Sˣ), f = α • g
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : M)
-- Lean 4 proof step from Mathlib.Algebra.Central.End (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
h_1 : Nontrivial M
α : S
hα : (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
β : S
hβ : (⇑g : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) β (⇑f : (a : M) → M₂)
x : M
hx : x ≠ 0
⊢ ∃ (α : Sˣ), f = α • g
have this : HSMul.hSMul.{u_4, u_5, u_5} (α := S) (β := M₂) 1 ((f : (a : M) → M₂) x : M₂) =
  HSMul.hSMul (β := M₂) (α * β) ((f : (a : M) → M₂) x : M₂)
Tactic: have : (1 : S) • f x = (α * β) • f x := by simpa [hβ, smul_smul] using congr($hα x)
-- Lean 4 proof step from Mathlib.Algebra.Central.End (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
h_1 : Nontrivial M
α : S
hα : (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
β : S
hβ : (⇑g : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) β (⇑f : (a : M) → M₂)
x : M
hx : x ≠ 0
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := S) (β := M₂) 1 ((f : (a : M) → M₂) x : M₂) =
    HSMul.hSMul (β := M₂) (α * β) ((f : (a : M) → M₂) x : M₂)
⊢ ∃ (α : Sˣ), f = α • g
have this₁ : 1 = α * β
Tactic: rw [smul_left_inj (by simpa)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
x : B ⊗[K] C
hx : Membership.mem (γ := Subalgebra K (B ⊗[K] C)) (Subalgebra.map includeLeft (Subalgebra.center K B)) x
⊢ Membership.mem (γ := Subalgebra K (B ⊗[K] C)) (Subalgebra.center K (B ⊗[K] C)) x
have simp : ∀ (hx : ∃ (x_1 : B), (∀ (b : B), b * x_1 = x_1 * b) ∧ (includeLeft : (a : B) → B ⊗[K] C) x_1 = x) (b : B ⊗[K] C),
  b * x = x * b
Tactic: simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
x : B ⊗[K] C
hx : ∃ (x_1 : B), (∀ (b : B), b * x_1 = x_1 * b) ∧ (includeLeft : (a : B) → B ⊗[K] C) x_1 = x
⊢ ∀ (b : B ⊗[K] C), b * x = x * b
have obtain : ∀ (b : B) (hb0 : ∀ (b_1 : B), b_1 * b = b * b_1) (b_1 : B ⊗[K] C),
  HMul.hMul (β := B ⊗[K] C) b_1 ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) b_1
Tactic: obtain ⟨b, hb0, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
bc : B ⊗[K] C
⊢ HMul.hMul (β := B ⊗[K] C) bc ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) bc
have zero : HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (0 : B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) (0 : B ⊗[K] C)
Tactic: induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b' c => simp [hb0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
bc : B ⊗[K] C
zero :
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (0 : B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) (0 : B ⊗[K] C)
⊢ HMul.hMul (β := B ⊗[K] C) bc ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) bc
have tmul : ∀ (b' : B) (c : C),
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (b' ⊗ₜ[K] c) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) (b' ⊗ₜ[K] c)
Tactic: induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b' c => simp [hb0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
bc : B ⊗[K] C
zero :
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (0 : B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) (0 : B ⊗[K] C)
tmul :
  ∀ (b' : B) (c : C),
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (b' ⊗ₜ[K] c) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
      HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) (b' ⊗ₜ[K] c)
⊢ HMul.hMul (β := B ⊗[K] C) bc ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) bc
have add : ∀ (x y : B ⊗[K] C),
  HMul.hMul (β := B ⊗[K] C) x ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
      HMul.hMul (α := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) x →
    HMul.hMul (β := B ⊗[K] C) y ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
        HMul.hMul (α := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) y →
      HMul.hMul (β := B ⊗[K] C) (x + y) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) =
        HMul.hMul (α := B ⊗[K] C) ((includeLeft : (a : B) → B ⊗[K] C) b : B ⊗[K] C) (x + y)
Tactic: induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b' c => simp [hb0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
x : B ⊗[K] C
hx : Membership.mem (γ := Subalgebra K (B ⊗[K] C)) (Subalgebra.map includeRight (Subalgebra.center K C)) x
⊢ Membership.mem (γ := Subalgebra K (B ⊗[K] C)) (Subalgebra.center K (B ⊗[K] C)) x
have simp : ∀ (hx : ∃ (x_1 : C), (∀ (b : C), b * x_1 = x_1 * b) ∧ (includeRight : (a : C) → B ⊗[K] C) x_1 = x) (b : B ⊗[K] C),
  b * x = x * b
Tactic: simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
x : B ⊗[K] C
hx : ∃ (x_1 : C), (∀ (b : C), b * x_1 = x_1 * b) ∧ (includeRight : (a : C) → B ⊗[K] C) x_1 = x
⊢ ∀ (b : B ⊗[K] C), b * x = x * b
have obtain : ∀ (c : C) (hc0 : ∀ (b : C), b * c = c * b) (b : B ⊗[K] C),
  HMul.hMul (β := B ⊗[K] C) b ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) b
Tactic: obtain ⟨c, hc0, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
bc : B ⊗[K] C
⊢ HMul.hMul (β := B ⊗[K] C) bc ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) bc
have zero : HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (0 : B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) (0 : B ⊗[K] C)
Tactic: induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
bc : B ⊗[K] C
zero :
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (0 : B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) (0 : B ⊗[K] C)
⊢ HMul.hMul (β := B ⊗[K] C) bc ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) bc
have tmul : ∀ (b : B) (c' : C),
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (b ⊗ₜ[K] c') ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) (b ⊗ₜ[K] c')
Tactic: induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.Central.TensorProduct (goal)
Goal:
K : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring K
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra K B
inst_4 : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
bc : B ⊗[K] C
zero :
  HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (0 : B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) (0 : B ⊗[K] C)
tmul :
  ∀ (b : B) (c' : C),
    HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) (b ⊗ₜ[K] c') ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
      HMul.hMul (α := B ⊗[K] C) (β := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) (b ⊗ₜ[K] c')
⊢ HMul.hMul (β := B ⊗[K] C) bc ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
    HMul.hMul (α := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) bc
have add : ∀ (x y : B ⊗[K] C),
  HMul.hMul (β := B ⊗[K] C) x ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
      HMul.hMul (α := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) x →
    HMul.hMul (β := B ⊗[K] C) y ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
        HMul.hMul (α := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) y →
      HMul.hMul (β := B ⊗[K] C) (x + y) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) =
        HMul.hMul (α := B ⊗[K] C) ((includeRight : (a : C) → B ⊗[K] C) c : B ⊗[K] C) (x + y)
Tactic: induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP A q
⊢ q ∣ p
have refine : Eq.{u_2 + 1} (α := A) (↑p : A) 0
Tactic: refine (CharP.cast_eq_zero_iff A q p).mp ?_
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP A q
⊢ Eq.{u_2 + 1} (α := A) (↑p : A) 0
have rw : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) (↑p : R) : A) (0 : A)
Tactic: rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP A q
rw : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) (↑p : R) : A) (0 : A)
⊢ Eq.{u_2 + 1} (α := A) (↑p : A) 0
have rw₁ : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) 0 : A) (0 : A)
Tactic: rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP A q
rw : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) (↑p : R) : A) (0 : A)
rw₁ : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) 0 : A) (0 : A)
⊢ Eq.{u_2 + 1} (α := A) (↑p : A) 0
have rw₂ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : NonAssocSemiring A
inst_3 : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst_4 : CharP R p
⊢ CharP A p
have this : Nontrivial R
Tactic: have := f.domain_nontrivial
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : NonAssocSemiring A
inst_3 : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst_4 : CharP R p
this : Nontrivial R
⊢ CharP A p
have H : Nat.Prime p
Tactic: have H := (CharP.char_is_prime_or_zero R p).resolve_right hp
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : NonAssocSemiring A
inst_3 : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst_4 : CharP R p
this : Nontrivial R
H : Nat.Prime p
⊢ CharP A p
have obtain : ∀ (q : ℕ) (hq : CharP A q), CharP A p
Tactic: obtain ⟨q, hq⟩ := CharP.exists A
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : NonAssocSemiring A
inst_3 : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst_4 : CharP R p
this : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
⊢ CharP A p
have obtain : ∀ (k : ℕ) (e : p = q * k), CharP A p
Tactic: obtain ⟨k, e⟩ := dvd_of_ringHom f p q
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : NonAssocSemiring A
inst_3 : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst_4 : CharP R p
this : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q * k
⊢ CharP A p
have this₁ : k = 1
Tactic: have := Nat.isUnit_iff.mp ((H.2 e).resolve_left (Nat.isUnit_iff.not.mpr (char_ne_one A q)))
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : NonAssocSemiring A
inst_3 : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst_4 : CharP R p
this_1 : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q * k
this : k = 1
⊢ CharP A p
have e₁ : p = q
Tactic: rw [this, mul_one] at e
Cleared hypotheses: e, this
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 : CharP R p
x : ℕ
⊢ Eq.{u_2 + 1} (α := A) (↑x : A) 0 ↔ p ∣ x
have rw : Eq.{u_2 + 1} (α := A) (↑x : A) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
Tactic: rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 : CharP R p
x : ℕ
rw : Eq.{u_2 + 1} (α := A) (↑x : A) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ Eq.{u_2 + 1} (α := A) (↑x : A) 0 ↔ p ∣ x
have rw₁ : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) (↑x : R) : A) (0 : A) ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
Tactic: rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 : CharP R p
x : ℕ
rw : Eq.{u_2 + 1} (α := A) (↑x : A) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
rw₁ : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) (↑x : R) : A) (0 : A) ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ Eq.{u_2 + 1} (α := A) (↑x : A) 0 ↔ p ∣ x
have rw₂ : Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
Tactic: rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 : CharP A p
⊢ CharP R p
have obtain : ∀ (q : ℕ) (h : CharP R q), CharP R p
Tactic: obtain ⟨q, h⟩ := CharP.exists R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
q : ℕ
hR : ExpChar R q
⊢ ExpChar A q
have zero : ∀ [CharZero R], ExpChar A 1
Tactic: rcases hR with _ | hprime
Cleared hypotheses: q, hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
q : ℕ
hR : ExpChar R q
zero : ∀ [CharZero R], ExpChar A 1
⊢ ExpChar A q
have prime : ∀ (hprime : Nat.Prime q) [CharP R q], ExpChar A q
Tactic: rcases hR with _ | hprime
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero R
⊢ ExpChar A 1
have this : CharZero A
Tactic: haveI := charZero_of_injective_ringHom h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
q : ℕ
hprime : Nat.Prime q
hchar : CharP R q
⊢ ExpChar A q
have this : CharP A q
Tactic: haveI := charP_of_injective_ringHom h q
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero A
⊢ ExpChar R 1
have this : CharZero R
Tactic: haveI := f.charZero
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
hp : Nat.Prime p
hchar : CharP A p
⊢ ExpChar R p
have this : CharP R p
Tactic: haveI := f.charP H p
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 cases : ExpChar A p
⊢ ExpChar R p
have zero : ∀ [CharZero A], ExpChar R 1
Tactic: cases ‹ExpChar A p› with
  | zero => haveI := f.charZero; exact .zero
  | prime hp => haveI := f.charP H p; exact .prime hp
Cleared hypotheses: p, inst_2
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 cases : ExpChar A p
zero : ∀ [CharZero A], ExpChar R 1
⊢ ExpChar R p
have prime : ∀ (hp : Nat.Prime p) [CharP A p], ExpChar R p
Tactic: cases ‹ExpChar A p› with
  | zero => haveI := f.charZero; exact .zero
  | prime hp => haveI := f.charP H p; exact .prime hp
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Algebra.CharP.Algebra (goal)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : CommSemiring L
inst_2 : Nontrivial L
inst_3 : Algebra K L
⊢ ringChar K = ringChar L
have rw : CharP L (ringChar L)
Tactic: rw [ringChar.eq_iff, Algebra.charP_iff K L]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
have inr : ∀
  (this :
    ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) (hle : a ≤ b),
      Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R))
  (hle : ¬a ≤ b), Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
Tactic: wlog hle : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
inr :
  ∀
    (this :
      ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) (hle : a ≤ b),
        Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R))
    (hle : ¬a ≤ b), Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
have wlog : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) (hle : a ≤ b),
  Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
Tactic: wlog hle : a ≤ b
Cleared hypotheses: inst_1, h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : AddMonoidWithOne R_1
p_1 a_1 b_1 : ℕ
R : Type u_1
inst_1 : AddMonoidWithOne R
p : ℕ
inst_2 : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
have h₁ : p ∣ b - a
Tactic: rw [Nat.modEq_iff_dvd' hle] at h
Cleared hypotheses: h, hle