awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
apply :
  ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
apply₁ :
  ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)
apply₂ :
  ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * (y + z))
apply₃ :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x * y)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
have apply₄ : ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
  (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
  Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * r • y)
Tactic: apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
have a : ∀ (x : A) (hx : x ∈ s), Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
Tactic: induction hx using adjoin_induction with
    | mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | add x y _ _ hpx hpy => exact add_mem hpx hpy
    | zero => exact zero_mem _
    | mul x y _ _ hpx hpy =>
      apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
      case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | smul r x _ hpx => exact smul_mem _ _ hpx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) x
a : ∀ (x : A) (hx : x ∈ s), Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
have a₁ : ∀ (x y : A),
  Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
      ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
        (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x + y)
Tactic: induction hx using adjoin_induction with
    | mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | add x y _ _ hpx hpy => exact add_mem hpx hpy
    | zero => exact zero_mem _
    | mul x y _ _ hpx hpy =>
      apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
      case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | smul r x _ hpx => exact smul_mem _ _ hpx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) x
a : ∀ (x : A) (hx : x ∈ s), Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
a₁ :
  ∀ (x y : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
        ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
          (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
          Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x + y)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
have a₂ : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) 0
Tactic: induction hx using adjoin_induction with
    | mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | add x y _ _ hpx hpy => exact add_mem hpx hpy
    | zero => exact zero_mem _
    | mul x y _ _ hpx hpy =>
      apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
      case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | smul r x _ hpx => exact smul_mem _ _ hpx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) x
a : ∀ (x : A) (hx : x ∈ s), Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
a₁ :
  ∀ (x y : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
        ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
          (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
          Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x + y)
a₂ : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) 0
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
have a₃ : ∀ (x y : A),
  Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
      ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
        (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
Tactic: induction hx using adjoin_induction with
    | mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | add x y _ _ hpx hpy => exact add_mem hpx hpy
    | zero => exact zero_mem _
    | mul x y _ _ hpx hpy =>
      apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
      case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | smul r x _ hpx => exact smul_mem _ _ hpx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) x
a : ∀ (x : A) (hx : x ∈ s), Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
a₁ :
  ∀ (x y : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
        ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
          (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
          Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x + y)
a₂ : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) 0
a₃ :
  ∀ (x y : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y →
        ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
          (hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
          Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
have a₄ : ∀ (r : R) (x : A),
  Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
    ∀ (hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x),
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x)
Tactic: induction hx using adjoin_induction with
    | mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | add x y _ _ hpx hpy => exact add_mem hpx hpy
    | zero => exact zero_mem _
    | mul x y _ _ hpx hpy =>
      apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
      case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | smul r x _ hpx => exact smul_mem _ _ hpx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
⊢ LE.le (α := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (NonUnitalSubalgebra.toSubmodule (adjoin R s))
have apply : (↑(Subsemigroup.closure s) : Set A) ⊆ (↑(NonUnitalSubalgebra.toSubmodule (adjoin R s)) : Set A)
Tactic: apply span_le.2 _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (adjoin R ⊥) ⊥
have gc : GaloisConnection (β := NonUnitalSubalgebra R A) (adjoin R) SetLike.coe
Tactic: apply GaloisConnection.l_bot
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
gc : GaloisConnection (β := NonUnitalSubalgebra R A) (adjoin R) SetLike.coe
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (adjoin R ⊥) ⊥
have u : NonUnitalSubalgebra R A → Set A
Tactic: apply GaloisConnection.l_bot
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
ι : Sort u_2
inst_9 : Nonempty ι
inst_10 : IsScalarTower R B B
inst_11 : SMulCommClass R B B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : ι → NonUnitalSubalgebra R A
⊢ Eq (α := NonUnitalSubalgebra R B) (NonUnitalSubalgebra.map f (⨅ (i : ι), S i))
    (⨅ (i : ι), NonUnitalSubalgebra.map f (S i))
have a : (↑(NonUnitalSubalgebra.map f (⨅ (i : ι), S i)) : Set B) = (↑(⨅ (i : ι), NonUnitalSubalgebra.map f (S i)) : Set B)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure ∅) : Set A)) x ↔ x = 0
have rw : Membership.mem (γ := Submodule R A) (Submodule.span R (↑⊥ : Set A)) x ↔ x = 0
Tactic: rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot,
      Submodule.span_zero_singleton, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
rw : Membership.mem (γ := Submodule R A) (Submodule.span R (↑⊥ : Set A)) x ↔ x = 0
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure ∅) : Set A)) x ↔ x = 0
have rw₁ : Membership.mem (γ := Submodule R A) (R ∙ 0) x ↔ x = 0
Tactic: rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot,
      Submodule.span_zero_singleton, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
rw : Membership.mem (γ := Submodule R A) (Submodule.span R (↑⊥ : Set A)) x ↔ x = 0
rw₁ : Membership.mem (γ := Submodule R A) (R ∙ 0) x ↔ x = 0
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure ∅) : Set A)) x ↔ x = 0
have rw₂ : Membership.mem (γ := Submodule R A) ⊥ x ↔ x = 0
Tactic: rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot,
      Submodule.span_zero_singleton, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
rw : Membership.mem (γ := Submodule R A) (Submodule.span R (↑⊥ : Set A)) x ↔ x = 0
rw₁ : Membership.mem (γ := Submodule R A) (R ∙ 0) x ↔ x = 0
rw₂ : Membership.mem (γ := Submodule R A) ⊥ x ↔ x = 0
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure ∅) : Set A)) x ↔ x = 0
have rw₃ : x = 0 ↔ x = 0
Tactic: rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot,
      Submodule.span_zero_singleton, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq.{v + 1} (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule ⊥) ⊥
have h : ∀ (x : A),
  Membership.mem (γ := Submodule R A) (NonUnitalSubalgebra.toSubmodule ⊥) x ↔ Membership.mem (γ := Submodule R A) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S
have rw : Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤
have h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : IsScalarTower R B B
inst_8 : SMulCommClass R B B
⊢ Eq (α := NonUnitalSubalgebra R (A × B)) (prod ⊤ ⊤) ⊤
have h : ∀ (x : A × B),
  Membership.mem (γ := NonUnitalSubalgebra R (A × B)) (prod ⊤ ⊤) x ↔
    Membership.mem (γ := NonUnitalSubalgebra R (A × B)) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
ι : Sort u_2
inst_5 : Nonempty ι
S : ι → NonUnitalSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative.{v} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{v} ↥(⨆ (i : ι), S i)
have this : IsMulCommutative.{v} ↥(⨆ (i : ι), (S i).toNonUnitalSubsemiring)
Tactic: have := NonUnitalSubsemiring.isMulCommutative_iSup dir
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
⊢ NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥T) B
have subst : NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(iSup K)) B
Tactic: subst hT
Cleared hypotheses: T, hT
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
⊢ Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))
have let : ∀ (k : ι) (hik : K i ≤ K k) (hjk : K j ≤ K k),
  Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))
Tactic: let ⟨k, hik, hjk⟩ := dir i j