awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Central.End
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
⊢ 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)
-- Module: Mathlib.Algebra.Central.End
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₂)
⊢ Ne.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)

Tactic:
simpa
-- Module: Mathlib.Algebra.Central.End
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₂)
⊢ 1 = α * β

Tactic:
rw [smul_left_inj (by simpa)] at this

Premises used: smul_left_inj
-- Module: Mathlib.Algebra.Central.End
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 : 1 = α * β
x_1 : M
⊢ Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) x_1 : M₂)
    (({ val := α, inv := β, val_inv := ⋯, inv_val := ⋯ : Sˣ } • g : (a : M) → M₂) x_1 : M₂)

Tactic:
simpa using congr($hα _)
-- Module: Mathlib.Algebra.Central.End
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 : 1 = α * β
⊢ ∃ (α : Sˣ), f = α • g

Tactic:
exact ⟨.mk α β this.symm (mul_comm α β ▸ this.symm), ext fun _ ↦ by simpa using congr($hα _)⟩
-- Module: Mathlib.Algebra.Central.Matrix
Goal:
n : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Fintype n
inst_4 : DecidableEq n
⊢ Eq (α := Subalgebra R (Matrix n n A)) (Subalgebra.center R (Matrix n n A))
    (Subalgebra.map (scalarAlgHom n R) (Subalgebra.center R A))

Tactic:
SetLike.coe_injective center_eq_scalar_image

Premises used: SetLike.coe_injective, Matrix.center_eq_scalar_image
-- Module: Mathlib.Algebra.Central.TensorProduct
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
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
⊢ Membership.mem (γ := Subalgebra K (B ⊗[K] C)) (Subalgebra.center K (B ⊗[K] C)) x

Tactic:
simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢

Premises used: Subalgebra.mem_center_iff, Subalgebra.mem_map
-- Module: Mathlib.Algebra.Central.TensorProduct
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
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
⊢ ∀ (b : B ⊗[K] C), b * x = x * b

Tactic:
obtain ⟨b, hb0, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Algebra.Central.TensorProduct
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.Central.TensorProduct
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
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:
simp [hb0]
-- Module: Mathlib.Algebra.Central.TensorProduct
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
x y : B ⊗[K] C
h :
  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
h_1 :
  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:
simp_all [add_mul, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Central.TensorProduct
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)
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)
⊢ 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

Tactic:
induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b' c => simp [hb0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]

Premises used: add_mul, mul_add, TensorProduct.tmul
-- Module: Mathlib.Algebra.Central.TensorProduct
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
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
⊢ Membership.mem (γ := Subalgebra K (B ⊗[K] C)) (Subalgebra.center K (B ⊗[K] C)) x

Tactic:
simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢

Premises used: Subalgebra.mem_center_iff, Subalgebra.mem_map
-- Module: Mathlib.Algebra.Central.TensorProduct
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
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
⊢ ∀ (b : B ⊗[K] C), b * x = x * b

Tactic:
obtain ⟨c, hc0, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Algebra.Central.TensorProduct
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.Central.TensorProduct
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
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:
simp [hc0]
-- Module: Mathlib.Algebra.Central.TensorProduct
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
x y : B ⊗[K] C
h :
  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
h_1 :
  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:
simp_all [add_mul, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Central.TensorProduct
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')
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)
⊢ 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

Tactic:
induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]

Premises used: add_mul, mul_add, TensorProduct.tmul
-- Module: Mathlib.Algebra.Central.TensorProduct
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
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := K) (β := B) (⇑(algebraMap K B) : (a : K) → B)
inst_5 : Module.Flat K C
inst_6 : IsCentral K (B ⊗[K] C)
⊢ IsCentral K C

Tactic:
have : IsCentral K (C ⊗[K] B) := IsCentral.of_algEquiv K _ _ <| Algebra.TensorProduct.comm _ _ _
  left_of_tensor K C B inj

Premises used: Algebra.IsCentral.of_algEquiv, Algebra.TensorProduct.comm, TensorProduct, Algebra.IsCentral.left_of_tensor
-- Module: Mathlib.Algebra.Central.TensorProduct
Goal:
K : Type u_4
B : Type u_5
C : Type u_6
inst : Field K
inst_1 : Ring B
inst_2 : Ring C
inst_3 : Nontrivial C
inst_4 : Algebra K B
inst_5 : Algebra K C
inst_6 : IsCentral K (B ⊗[K] C)
⊢ IsCentral K B

Tactic:
left_of_tensor K B C <| FaithfulSMul.algebraMap_injective K C

Premises used: FaithfulSMul.algebraMap_injective, Algebra.IsCentral.left_of_tensor
-- Module: Mathlib.Algebra.Central.TensorProduct
Goal:
K : Type u_4
B : Type u_5
C : Type u_6
inst : Field K
inst_1 : Ring B
inst_2 : Ring C
inst_3 : Nontrivial B
inst_4 : Algebra K B
inst_5 : Algebra K C
inst_6 : IsCentral K (B ⊗[K] C)
⊢ IsCentral K C

Tactic:
right_of_tensor K B C <| FaithfulSMul.algebraMap_injective K B

Premises used: Algebra.IsCentral.right_of_tensor, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.CharP.Algebra
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

Tactic:
(CharP.cast_eq_zero_iff A q p).mp ?_

Premises used: Iff.mp, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Algebra
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
refine : Eq.{u_2 + 1} (α := A) (↑p : A) 0
⊢ q ∣ p

Tactic:
refine (CharP.cast_eq_zero_iff A q p).mp ?_

Premises used: Iff.mp, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Algebra
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)
rw₂ rw₃ : Eq.{u_2 + 1} (α := A) 0 0
⊢ Eq.{u_2 + 1} (α := A) (↑p : A) 0

Tactic:
rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]

Premises used: CharP.cast_eq_zero, map_zero, map_natCast
-- Module: Mathlib.Algebra.CharP.Algebra
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
⊢ Nontrivial R

Tactic:
have := f.domain_nontrivial
-- Module: Mathlib.Algebra.CharP.Algebra
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
⊢ Nat.Prime p

Tactic:
have H := (CharP.char_is_prime_or_zero R p).resolve_right hp
-- Module: Mathlib.Algebra.CharP.Algebra
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
obtain : ∀ (q : ℕ) (hq : CharP A q), CharP A p
⊢ CharP A p

Tactic:
obtain ⟨q, hq⟩ := CharP.exists A

Premises used: CharP.exists
-- Module: Mathlib.Algebra.CharP.Algebra
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
obtain : ∀ (k : ℕ) (e : p = q * k), CharP A p
⊢ CharP A p

Tactic:
obtain ⟨k, e⟩ := dvd_of_ringHom f p q

Premises used: CharP.dvd_of_ringHom
-- Module: Mathlib.Algebra.CharP.Algebra
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
⊢ k = 1

Tactic:
have := Nat.isUnit_iff.mp ((H.2 e).resolve_left (Nat.isUnit_iff.not.mpr (char_ne_one A q)))
-- Module: Mathlib.Algebra.CharP.Algebra
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
⊢ p = q

Tactic:
rw [this, mul_one] at e

Premises used: mul_one
-- Module: Mathlib.Algebra.CharP.Algebra
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
e₁ : p = q
⊢ k = 1

Tactic:
rw [this, mul_one] at e

Premises used: mul_one
-- Module: Mathlib.Algebra.CharP.Algebra
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
this : k = 1
⊢ CharP A p

Tactic:
e ▸ hq

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.CharP.Algebra
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
this : k = 1
⊢ CharP A p

Tactic:
exact e ▸ hq
-- Module: Mathlib.Algebra.CharP.Algebra
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ Eq.{u_2 + 1} (α := A) (↑x : A) 0 ↔ p ∣ x

Tactic:
rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]

Premises used: map_natCast, map_eq_zero_iff, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p : ℕ
inst_3 : CharP R p
⊢ CharP A p

Tactic:
charP_of_injective_ringHom h p

Premises used: charP_of_injective_ringHom
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
A : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
p : ℕ
inst_4 : CharP R p
⊢ CharP A p

Tactic:
charP_of_injective_ringHom (FaithfulSMul.algebraMap_injective R A) p

Premises used: charP_of_injective_ringHom, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.CharP.Algebra
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
x x_1 : ℕ
h_1 : Eq.{u_2 + 1} (α := A) (↑x : A) (↑x_1 : A)
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) (↑x : R) : A) ((f : (a : R) → A) (↑x_1 : R) : A)

Tactic:
simpa only [map_natCast f]

Premises used: map_natCast
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
inst_3 : CharZero R
⊢ CharZero A

Tactic:
charZero_of_injective_ringHom h

Premises used: charZero_of_injective_ringHom
-- Module: Mathlib.Algebra.CharP.Algebra
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
obtain : ∀ (q : ℕ) (h : CharP R q), CharP R p
⊢ CharP R p

Tactic:
obtain ⟨q, h⟩ := CharP.exists R

Premises used: CharP.exists
-- Module: Mathlib.Algebra.CharP.Algebra
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
q : ℕ
h : CharP R q
⊢ CharP R p

Tactic:
CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h

Premises used: charP_of_injective_ringHom, Eq.rec, CharP.eq