awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x * y)
have rw₂ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
rw₂ :
  HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x * y)
have rw₃ : HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
rw₂ :
  HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₃ :
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x * y)
have rw₄ : HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B) =
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x + y)
have rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x + y)
have rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x + y)
have rw₂ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
rw₂ :
  HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x + y)
have rw₃ : HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
rw₂ :
  HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₃ :
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x + y)
have rw₄ : HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B) =
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S
have mk : ∀ (toSubsemiring : Subsemiring A)
  (algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)),
  { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' :
            Subalgebra R A }.toNonUnitalSubalgebra.toSubalgebra
      sorry =
    { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' }
Tactic: cases S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toSubalgebra h1).toNonUnitalSubalgebra = S
have mk : ∀ (toNonUnitalSubsemiring : NonUnitalSubsemiring A)
  (smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier)
  (h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' : NonUnitalSubalgebra R A }),
  ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' : NonUnitalSubalgebra R A }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' }
Tactic: cases S
Cleared hypotheses: S, h1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
S T K : Subalgebra R A
⊢ K ≤ centralizer R (↑(S ⊔ T) : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
have simp_rw : S ⊔ T ≤ centralizer R (↑K : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
Tactic: simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
S T K : Subalgebra R A
simp_rw : S ⊔ T ≤ centralizer R (↑K : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
⊢ K ≤ centralizer R (↑(S ⊔ T) : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
have simp_rw₁ : S ≤ centralizer R (↑K : Set A) ∧ T ≤ centralizer R (↑K : Set A) ↔
  K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
Tactic: simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
S T K : Subalgebra R A
simp_rw : S ⊔ T ≤ centralizer R (↑K : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
simp_rw₁ :
  S ≤ centralizer R (↑K : Set A) ∧ T ≤ centralizer R (↑K : Set A) ↔
    K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
⊢ K ≤ centralizer R (↑(S ⊔ T) : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
have simp_rw₂ : S ≤ centralizer R (↑K : Set A) ∧ T ≤ centralizer R (↑K : Set A) ↔
  K ≤ centralizer R (↑S : Set A) ∧ K ≤ centralizer R (↑T : Set A)
Tactic: simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_3
S : ι → Subalgebra R A
K : Subalgebra R A
⊢ K ≤ centralizer R (↑(⨆ (i : ι), S i) : Set A) ↔ K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
have simp_rw : LE.le (α := Subalgebra R A) (⨆ (i : ι), S i) (centralizer R (↑K : Set A)) ↔
  K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
Tactic: simp_rw [le_centralizer_iff, iSup_le_iff, le_iInf_iff, K.le_centralizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_3
S : ι → Subalgebra R A
K : Subalgebra R A
simp_rw :
  LE.le (α := Subalgebra R A) (⨆ (i : ι), S i) (centralizer R (↑K : Set A)) ↔
    K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
⊢ K ≤ centralizer R (↑(⨆ (i : ι), S i) : Set A) ↔ K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
have simp_rw₁ : (∀ (i : ι), S i ≤ centralizer R (↑K : Set A)) ↔ K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
Tactic: simp_rw [le_centralizer_iff, iSup_le_iff, le_iInf_iff, K.le_centralizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_3
S : ι → Subalgebra R A
K : Subalgebra R A
simp_rw :
  LE.le (α := Subalgebra R A) (⨆ (i : ι), S i) (centralizer R (↑K : Set A)) ↔
    K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
simp_rw₁ : (∀ (i : ι), S i ≤ centralizer R (↑K : Set A)) ↔ K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
⊢ K ≤ centralizer R (↑(⨆ (i : ι), S i) : Set A) ↔ K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
have simp_rw₂ : (∀ (i : ι), S i ≤ centralizer R (↑K : Set A)) ↔ ∀ (i : ι), K ≤ centralizer R (↑(S i) : Set A)
Tactic: simp_rw [le_centralizer_iff, iSup_le_iff, le_iInf_iff, K.le_centralizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
have h : ∀ (w : A ⊗[R] B),
  Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w ↔
    Membership.mem (γ := Subalgebra R (A ⊗[R] B))
      (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
          (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
            TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
        Subalgebra R (A ⊗[R] B))
      w
Tactic: ext w
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
w : A ⊗[R] B
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w ↔
    Membership.mem (γ := Subalgebra R (A ⊗[R] B))
      (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
          (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
            TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
        Subalgebra R (A ⊗[R] B))
      w
have h : Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w →
  Membership.mem (γ := Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
    w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
w : A ⊗[R] B
h :
  Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w →
    Membership.mem (γ := Subalgebra R (A ⊗[R] B))
      (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
          (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
            TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
        Subalgebra R (A ⊗[R] B))
      w
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w ↔
    Membership.mem (γ := Subalgebra R (A ⊗[R] B))
      (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
          (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
            TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
        Subalgebra R (A ⊗[R] B))
      w
have h₁ : Membership.mem (γ := Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
    w →
  Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
w : A ⊗[R] B
hw : Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
    w
have hw₁ : ∀ (g : A ⊗[R] B), Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g → g * w = w * g
Tactic: rw [mem_centralizer_iff] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
w : A ⊗[R] B
hw : ∀ (g : A ⊗[R] B), Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g → g * w = w * g
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
    w
have h : ∀ (b : Finsupp.{u_3, u_2} (Module.Free.ChooseBasisIndex R B) A)
  (hw :
    ∀ (g : A ⊗[R] B),
      Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g →
        (g *
            b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
              m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) =
          (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
              m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) *
            g),
  Membership.mem (γ := Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
    (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
      m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
Tactic: obtain ⟨b, rfl⟩ := TensorProduct.eq_repr_basis_right ℬ w
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Finsupp.{u_3, u_2} (Module.Free.ChooseBasisIndex R B) A
hw :
  ∀ (g : A ⊗[R] B),
    Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g →
      (g *
          b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
            m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) =
        (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
            m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) *
          g
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
    (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
      m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
have h : ∀ (j : Module.Free.ChooseBasisIndex R B) (hj : j ∈ b.support),
  Membership.mem (α := A) (γ := Subalgebra R A) (centralizer R S)
    ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j : A)
Tactic: refine Subalgebra.sum_mem _ fun j hj => ⟨⟨b j, ?_⟩ ⊗ₜ[R] ℬ j, by simp⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Finsupp.{u_3, u_2} (Module.Free.ChooseBasisIndex R B) A
hw :
  ∀ (g : A ⊗[R] B),
    Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g →
      (g *
          b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
            m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) =
        (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
            m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) *
          g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
⊢ HMul.hMul (β := A) x ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j : A) =
    HMul.hMul (α := A) ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j : A) x
have h : x • b = mapRange (fun (x_1 : A) ↦ x_1 * x) sorry b
Tactic: suffices x • b = b.mapRange (· * x) (by simp) from Finsupp.ext_iff.1 this j