awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
⊢ Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((((AlgebraTensorModule.curry
                  ((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
                        (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
                      M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) ∘ₗ
                    (comul : M ⊗[R] R →ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R))) :
                M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
              (a : M) → R →ₗ[R] M ⊗[S] M)
            x :
          LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
        (a : R) → M ⊗[S] M)
      1)
    (((((AlgebraTensorModule.curry (comul ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)) :
                M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
              (a : M) → R →ₗ[R] M ⊗[S] M)
            x :
          LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
        (a : R) → M ⊗[S] M)
      1)
have a : Eq.{u_7 + 1} (α := M ⊗[S] M)
  (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
            (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
          M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
        (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
      (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
            TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
          (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
        ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
    M ⊗[S] M)
  ((comul : (a : M) → M ⊗[S] M) (HSMul.hSMul.{u_5, u_7, u_7} (α := R) 1 x) : M ⊗[S] M)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
⊢ Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    ((comul : (a : M) → M ⊗[S] M) (HSMul.hSMul.{u_5, u_7, u_7} (α := R) 1 x) : M ⊗[S] M)
have a : Eq.{u_7 + 1} (α := M ⊗[S] M)
  (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
            (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
          M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
        (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
      (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
            TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
          (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
        ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
    M ⊗[S] M)
  ((comul : (a : M) → M ⊗[S] M) x : M ⊗[S] M)
Tactic: simp only [one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
⊢ Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    ((comul : (a : M) → M ⊗[S] M) x : M ⊗[S] M)
have a : ∀ (x₁ x₂ : M),
  Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    (x₁ ⊗ₜ[S] x₂ : M ⊗[S] M)
Tactic: hopf_tensor_induction comul (R := S) x with x₁ x₂
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
⊢ Eq (α := C →ₗ[R] R) (counit ∘ₗ δ) ε
have simp : Eq (α := C →ₗ[R] R)
  (((↑(_root_.TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ AlgebraTensorModule.map ε ε :
      LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id R) (C ⊗[R] C) R) ∘ₗ
    (δ : C →ₗ[R] C ⊗[R] C))
  ε
Tactic: simp only [counit_def, AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
⊢ Eq (α := C →ₗ[R] R) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ) ε
have h : ∀ (x : C), Eq.{u_5 + 1} (α := R) (((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ : (a : C) → R) x : R) ((ε : (a : C) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
⊢ Eq (α := C →ₗ[R] R)
    (((↑(_root_.TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ AlgebraTensorModule.map ε ε :
        LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id R) (C ⊗[R] C) R) ∘ₗ
      (δ : C →ₗ[R] C ⊗[R] C))
    ε
have _ : Eq (α := C →ₗ[R] R) ((μ ∘ₗ map ε ε) ∘ₗ δ) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ)
Tactic: calc
        (μ ∘ₗ (ε ⊗ₘ ε)) ∘ₗ δ
    _ = (μ ∘ₗ ε ▷ R) ∘ₗ (C ◁ ε ∘ₗ δ) := by simp [coassoc_simps]
    _ = ε := by ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
_ : Eq (α := C →ₗ[R] R) ((μ ∘ₗ map ε ε) ∘ₗ δ) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ)
⊢ Eq (α := C →ₗ[R] R)
    (((↑(_root_.TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ AlgebraTensorModule.map ε ε :
        LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id R) (C ⊗[R] C) R) ∘ₗ
      (δ : C →ₗ[R] C ⊗[R] C))
    ε
have _₁ : Eq (α := C →ₗ[R] R) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ) ε
Tactic: calc
        (μ ∘ₗ (ε ⊗ₘ ε)) ∘ₗ δ
    _ = (μ ∘ₗ ε ▷ R) ∘ₗ (C ◁ ε ∘ₗ δ) := by simp [coassoc_simps]
    _ = ε := by ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((leftMulMatrix basisOneI : (a : ℂ) → Matrix (Fin 2) (Fin 2) ℝ) z : Matrix (Fin 2) (Fin 2) ℝ)
    (!![z.re, -z.im; z.im, z.re] : Matrix (Fin 2) (Fin 2) ℝ)
have a : ∀ (i j : Fin 2),
  Eq (α := ℝ) ((leftMulMatrix basisOneI : (a : ℂ) → Matrix (Fin 2) (Fin 2) ℝ) z i j : ℝ)
    (!![z.re, -z.im; z.im, z.re] i j : ℝ)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i j : Fin 2
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    ![![z.re, -z.im], ![z.im, z.re]] i j
have a : ![z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).re -
        z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).im,
      z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).im +
        z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).re]
    i =
  ![![z.re, -z.im], ![z.im, z.re]] i ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i j : Fin 2
a :
  ![z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re -
          z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im,
        z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im +
          z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    ![![z.re, -z.im], ![z.im, z.re]] i j
have a₁ : ![z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).re -
        z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).im,
      z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).im +
        z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).re]
    i =
  ![![z.re, -z.im], ![z.im, z.re]] i ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i : Fin 2
⊢ ![z.re * re 1 - z.im * im 1, z.re * im 1 + z.im * re 1] i = ![![z.re, -z.im], ![z.im, z.re]] i 0
have a : ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0
Tactic: simp only [one_re, mul_one, one_im, mul_zero,
      sub_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i : Fin 2
⊢ ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0
have a : ![z.re, z.im] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) 0
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i : Fin 2
a :
  ![z.re, z.im] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 0
⊢ ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0
have a₁ : ![z.re, z.im] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) 0
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i : Fin 2
⊢ ![z.re * I.re - z.im * I.im, z.re * I.im + z.im * I.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1
have a : ![-z.im, z.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1
Tactic: simp only [I_re, mul_zero, I_im,
      mul_one, zero_sub, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i : Fin 2
⊢ ![-z.im, z.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1
have a : ![-z.im, z.re] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) 1
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
i : Fin 2
a :
  ![-z.im, z.re] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1
⊢ ![-z.im, z.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1
have a₁ : ![-z.im, z.re] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) 1
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
⊢ (trace ℝ ℂ : (a : ℂ) → ℝ) z = 2 * z.re
have rw : HAdd.hAdd (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 0 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 1 : ℝ) = 2 * z.re
Tactic: rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex,
    Matrix.trace_fin_two]
-- Lean 4 proof step from Mathlib.RingTheory.Complex (goal)
Goal:
z : ℂ
⊢ Eq (α := ℝ) ((norm ℝ : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)
have rw : HMul.hMul (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 0 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 1 : ℝ) -
    HMul.hMul (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 1 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 0 : ℝ) =
  z.re * z.re + z.im * z.im
Tactic: rw [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex,
    Matrix.det_fin_two, normSq_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
have inl : Subsingleton L →
  (Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)))
Tactic: cases subsingleton_or_nontrivial L
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
inl :
  Subsingleton L →
    (Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
      ∀ (z : S),
        Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
          (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)))
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
have inr : Nontrivial L →
  (Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)))
Tactic: cases subsingleton_or_nontrivial L
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Subsingleton L
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
have inl : Membership.mem (γ := Submodule S L) ⊤ y ↔
  ∀ (z : S), Membership.mem (γ := Subalgebra R L) ⊤ (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
Tactic: rw [Subsingleton.elim (coeSubmodule L _) ⊤, Subsingleton.elim (Algebra.adjoin R _) ⊤]
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Nontrivial L
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
have trans : Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
  ∀ (z : S),
    Membership.mem (γ := Subalgebra R L) (Subalgebra.map (IsScalarTower.toAlgHom R S L) R[x])
      (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
Tactic: trans ∀ z, y * (algebraMap S L) z ∈ (R[x]).map (IsScalarTower.toAlgHom R S L)
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Nontrivial L
trans :
  Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) (Subalgebra.map (IsScalarTower.toAlgHom R S L) R[x])
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
have trans₁ : (∀ (z : S),
    Membership.mem (γ := Subalgebra R L) (Subalgebra.map (IsScalarTower.toAlgHom R S L) R[x])
      (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))) ↔
  ∀ (z : S),
    Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
      (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
Tactic: trans ∀ z, y * (algebraMap S L) z ∈ (R[x]).map (IsScalarTower.toAlgHom R S L)
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Nontrivial L
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) (Subalgebra.map (IsScalarTower.toAlgHom R S L) R[x])
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
have simp : (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) ↔
  ∀ (z : S),
    ∃ (x_1 : S),
      Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
        (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)
Tactic: simp only [coeSubmodule, Submodule.mem_map, linearMap_apply, Subalgebra.mem_map,
      IsScalarTower.coe_toAlgHom']
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Nontrivial L
⊢ (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) ↔
    ∀ (z : S),
      ∃ (x_1 : S),
        Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
          (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)
have mp : (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) →
  ∀ (z : S),
    ∃ (x_1 : S),
      Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
        (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Nontrivial L
mp :
  (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) →
    ∀ (z : S),
      ∃ (x_1 : S),
        Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
          (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)
⊢ (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) ↔
    ∀ (z : S),
      ∃ (x_1 : S),
        Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
          (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)
have mpr : (∀ (z : S),
    ∃ (x_1 : S),
      Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
        (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)) →
  ∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y
Tactic: constructor