awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inl : Subsingleton R → Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inr : Nontrivial R → Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))

Tactic:
rcases subsingleton_or_nontrivial R with _ | _

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Subsingleton R
⊢ Subsingleton S

Tactic:
haveI := Module.subsingleton R S
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Subsingleton R
this : Subsingleton S
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
⊢ Nontrivial S

Tactic:
nontriviality S using rank_subsingleton'

Premises used: rank_subsingleton'
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
⊢ IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))

Tactic:
haveI : IsScalarTower R A (Algebra.adjoin A (B : Set S)) :=
    IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this_2 : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
this : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
rw : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))

Tactic:
rw [rank_mul_rank R A (Algebra.adjoin A (B : Set S))]

Premises used: rank_mul_rank, Algebra.adjoin, Membership.mem, Subtype, SetLike.coe
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this_2 : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
this : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
change : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(restrictScalars R (S := ↥A) (Algebra.adjoin ↥A (↑B : Set S)))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin ↥A (↑B : Set S))

Tactic:
change _ = Module.rank R ((Algebra.adjoin A (B : Set S)).restrictScalars R)

Premises used: Algebra.adjoin, Membership.mem, Subtype, SetLike.coe, Module.rank, Subalgebra.restrictScalars
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this_2 : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
this : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
rw : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin R ((↑A : Set S) ∪ (↑B : Set S)))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(restrictScalars R (S := ↥A) (Algebra.adjoin ↥A (↑B : Set S)))

Tactic:
rw [Algebra.restrictScalars_adjoin]

Premises used: Algebra.restrictScalars_adjoin
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this_2 : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
this : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin R ((↑A : Set S) ∪ (↑B : Set S)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ finrank.{u_1, u_2} R ↥(A ⊔ B) = finrank.{u_1, u_2} R ↥A * finrank.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))

Tactic:
simpa only [map_mul] using congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ finrank.{u_1, u_2} R ↥A ∣ finrank.{u_1, u_2} R ↥(A ⊔ B)

Tactic:
⟨_, finrank_sup_eq_finrank_left_mul_finrank_of_free A B⟩

Premises used: Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥B
inst_4 : Free.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
rw : Module.rank R ↥(B ⊔ A) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
rw₁ rw₂ :
  Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S)) =
    Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))

Tactic:
rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]

Premises used: Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free, sup_comm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥B
inst_4 : Free.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
rw : finrank.{u_1, u_2} R ↥(B ⊔ A) = finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
rw₁ rw₂ :
  finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S)) =
    finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
⊢ finrank.{u_1, u_2} R ↥(A ⊔ B) = finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))

Tactic:
rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]

Premises used: Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free, sup_comm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥B
inst_4 : Free.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
⊢ finrank.{u_1, u_2} R ↥B ∣ finrank.{u_1, u_2} R ↥(A ⊔ B)

Tactic:
⟨_, finrank_sup_eq_finrank_right_mul_finrank_of_free A B⟩

Premises used: Subalgebra.finrank_sup_eq_finrank_right_mul_finrank_of_free, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : R
⊢ Eq (α := Module.End R A)
    ((lmul R A : (a : A) → Module.End R A) ((algebraMap R A : (a : R) → A) x : A) : Module.End R A)
    ((lsmul R R A : (a : R) → Module.End R A) x : Module.End R A)

Tactic:
Eq.symm <| LinearMap.ext <| smul_def x

Premises used: LinearMap.ext, Algebra.smul_def, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
S₀ : Subalgebra R S
⊢ IsScalarTower (↥S₀) S A

Tactic:
of_algebraMap_eq fun _ ↦ rfl

Premises used: Set.Mem, IsScalarTower.of_algebraMap_eq, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
S₀ : Subalgebra R S
⊢ IsScalarTower.{u, v, w} R (↥S₀) A

Tactic:
@IsScalarTower.of_algebraMap_eq R S₀ A _ _ _ _ _ _ fun _ ↦
    (IsScalarTower.algebraMap_apply R S A _ :)

Premises used: Set.Mem, IsScalarTower.of_algebraMap_eq, IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra R A
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
U : Subalgebra S A
x : R
rw : Membership.mem (α := A) U.carrier ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
⊢ Membership.mem (α := A) U.carrier ((algebraMap R A : (a : R) → A) x : A)

Tactic:
rw [IsScalarTower.algebraMap_apply R S A]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra R A
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
U : Subalgebra S A
x : R
⊢ Membership.mem (α := A) U.carrier ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)

Tactic:
U.algebraMap_mem _

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra R A
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
U : Subalgebra S A
x : R
⊢ Membership.mem (α := A) U.carrier ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)

Tactic:
exact U.algebraMap_mem _

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
U : Subalgebra S A
⊢ (↑(restrictScalars R U) : Set A) = (↑U : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
⊢ (↑(restrictScalars.{u, v, w} R (S := S) ⊤) : Set A) = (↑⊤ : Set A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
U : Subalgebra S A
⊢ Eq (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) (restrictScalars R U) : Submodule R A)
    (Submodule.restrictScalars.{u, v, w} R (R := S) ((toSubmodule : (a : Subalgebra S A) → Submodule S A) U) :
      Submodule R A)

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
U : Subalgebra S A
x : A
⊢ Membership.mem (γ := Subalgebra R A) (restrictScalars R U) x ↔ x ∈ U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
U V : Subalgebra S A
H : Eq (α := Subalgebra R A) (restrictScalars R U) (restrictScalars R V)
x : A
rw : Membership.mem (γ := Subalgebra R A) (restrictScalars R U) x ↔ x ∈ V
rw₁ : Membership.mem (γ := Subalgebra R A) (restrictScalars R V) x ↔ x ∈ V
rw₂ rw₃ : x ∈ V ↔ x ∈ V
⊢ x ∈ U ↔ x ∈ V

Tactic:
rw [← mem_restrictScalars R, H, mem_restrictScalars]

Premises used: Subalgebra.mem_restrictScalars
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
h :
  ∀ (x : A),
    Membership.mem (γ := Submodule R A) (Submodule.restrictScalars R (R := ↥S) 1) x ↔
      Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
⊢ Eq.{w + 1} (α := Submodule R A) (Submodule.restrictScalars R (R := ↥S) 1)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
⊢ Membership.mem (γ := Submodule R A) (Submodule.restrictScalars R (R := ↥S) 1) x ↔
    Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ Codisjoint (α := Submodule (↥S) A) 1 (Submodule.restrictScalars (↥S) I) ↔
    Codisjoint (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      (Submodule.restrictScalars R I : Submodule R A)

Tactic:
simp [← Submodule.codisjoint_restrictScalars_iff R]

Premises used: Submodule.codisjoint_restrictScalars_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ Disjoint (α := Submodule (↥S) A) 1 (Submodule.restrictScalars (↥S) I) ↔
    Disjoint (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      (Submodule.restrictScalars R I : Submodule R A)

Tactic:
simp [← Submodule.disjoint_restrictScalars_iff R]

Premises used: Submodule.disjoint_restrictScalars_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
h :
  ∀ (x : A),
    Membership.mem (γ := Submodule R A)
        (LinearMap.range (M := ↥S) (τ₁₂ := RingHom.id R)
          (↑(toAlgHom R (↥S) A) :
            [inst_3 : FunLike (↥S →ₐ[R] A) (↥S) A] →
              [SemilinearMapClass (↥S →ₐ[R] A) (RingHom.id R) (↥S) A] → ↥S →ₗ[R] A))
        x ↔
      Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
⊢ Eq (α := Submodule R A)
    (LinearMap.range (M := ↥S) (τ₁₂ := RingHom.id R)
      (↑(toAlgHom R (↥S) A) :
        [inst_3 : FunLike (↥S →ₐ[R] A) (↥S) A] → [SemilinearMapClass (↥S →ₐ[R] A) (RingHom.id R) (↥S) A] → ↥S →ₗ[R] A))
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
⊢ Membership.mem (γ := Submodule R A)
      (LinearMap.range (M := ↥S) (τ₁₂ := RingHom.id R)
        (↑(toAlgHom R (↥S) A) :
          [inst_3 : FunLike (↥S →ₐ[R] A) (↥S) A] →
            [SemilinearMapClass (↥S →ₐ[R] A) (RingHom.id R) (↥S) A] → ↥S →ₗ[R] A))
      x ↔
    Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x

Tactic:
simp [algebraMap_eq]

Premises used: Subalgebra.algebraMap_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
t : Set A
z : A
⊢ Membership.mem (γ := Subsemiring A)
      (Subsemiring.closure
        (Set.range (ι := ↥(AlgHom.range (toAlgHom R S A)))
            (⇑(algebraMap (↥(AlgHom.range (toAlgHom R S A))) A) : (a : ↥(toAlgHom R S A).range) → A) ∪
          t))
      z ↔
    Membership.mem (γ := Subsemiring A)
      (Subsemiring.closure (Set.range.{w, v + 1} (ι := S) (⇑(algebraMap S A) : (a : S) → A) ∪ t)) z

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
⊢ AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S ↔
    NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
refine_1 :
  ∀ (h : AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S),
    NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
refine_2 :
  ∀ (h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra),
    AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S
⊢ AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S ↔
    NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S
x : A
⊢ Eq.{u_3 + 1} (α := C)
    ((AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) : (a : Unitization R A) → C)
        (↑x : Unitization R A) :
      C)
    ((f : (a : A) → C) x : C)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S
x : A
⊢ Membership.mem (α := C) S.toNonUnitalSubalgebra (((↑f : A →ₙ+* C) : (a : A) → C) x : C)

Tactic:
exact @h (f x) ⟨x, by simp⟩

Premises used: Unitization.inr, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
r : R
a : A
⊢ Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) : (a : Unitization R A) → C)
        (inl r + (↑a : Unitization R A)) :
      C)

Tactic:
simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)

Premises used: algebraMap_mem, Exists.intro, AddMemClass.add_mem, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
x : Unitization R A
refine_2 :
  ∀ (r : R) (a : A),
    Membership.mem (α := C) S
      ((AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) : (a : Unitization R A) → C)
          (inl r + (↑a : Unitization R A)) :
        C)
⊢ Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) : (a : Unitization R A) → C) x :
      C)

Tactic:
induction x with
    | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
rw : NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ (↑(NonUnitalAlgHom.range f) : Set C) ⊆ (↑c : Set C)
⊢ AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ c ↔
    Algebra.adjoin R (↑(NonUnitalAlgHom.range f) : Set C) ≤ c

Tactic:
rw [lift_range_le, Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff, Unitization.lift_range_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ (↑(NonUnitalAlgHom.range f) : Set C) ⊆ (↑c : Set C)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
x : Unitization.{u_1, u_3} R ↥s
⊢ (unitization s : (a : Unitization R ↥s) → A) x =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.toProd.1 : A) (↑x.toProd.2 : A)

Tactic:
rfl

Premises used: rfl