awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
y : Subalgebra R A
hy : y ∈ S
e_s : ∃ a ∈ S, Membership.mem (α := A) a ((algebraMap R A : (a : R) → A) x : A)
⊢ Membership.mem (α := A) (⋃₀ (SetLike.coe '' S)) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]

Premises used: Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe, Set.mem_sUnion
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ ∃ a ∈ S, Membership.mem (α := A) a ((algebraMap R A : (a : R) → A) x : A)

Tactic:
⟨y, hy, algebraMap_mem y x⟩

Premises used: And.intro, algebraMap_mem, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ ∃ a ∈ S, Membership.mem (α := A) a ((algebraMap R A : (a : R) → A) x : A)

Tactic:
exact ⟨y, hy, algebraMap_mem y x⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ (↑(⨅ (i : ι), S i) : Set A) = ⋂ (i : ι), (↑(S i) : Set A)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
x : A
⊢ Membership.mem (γ := Subalgebra R A) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Algebra.mem_sInf, Set.forall_mem_range
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
ι : Sort u_1
inst_5 : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
s : ι → Subalgebra R A
a : (↑(Subalgebra.map f (iInf s)) : Set B) = (↑(⨅ (i : ι), Subalgebra.map f (s i)) : Set B)
⊢ Subalgebra.map f (iInf s) = ⨅ (i : ι), Subalgebra.map f (s i)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
ι : Sort u_1
inst_5 : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
s : ι → Subalgebra R A
⊢ (↑(Subalgebra.map f (iInf s)) : Set B) = (↑(⨅ (i : ι), Subalgebra.map f (s i)) : Set B)

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, Set.injOn_of_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ (↑((toSubmodule : (a : Subalgebra R A) → Submodule R A) (⨅ (i : ι), S i) : Submodule R A) : Set A) =
    (↑(⨅ (i : ι), (toSubmodule : (a : Subalgebra R A) → Submodule R A) (S i)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ (iInf S).toSubsemiring = ⨅ (i : ι), (S i).toSubsemiring

Tactic:
simp only [iInf, sInf_toSubsemiring, ← Set.range_comp, Function.comp_def]

Premises used: Set.range_comp, iInf, Algebra.sInf_toSubsemiring, Function.comp_def
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
inst_3 : Nonempty ι
S : ι → Subalgebra R A
⊢ (iSup S).toSubsemiring = ⨆ (i : ι), (S i).toSubsemiring

Tactic:
simp only [iSup, Set.range_nonempty, sSup_toSubsemiring, ← Set.range_comp, Function.comp_def]

Premises used: Set.range_comp, iSup, Algebra.sSup_toSubsemiring, Function.comp_def, Set.range_nonempty
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
i : ι
x : A
hx : x ∈ S i
⊢ x ∈ iSup S

Tactic:
le_iSup S i hx

Premises used: Set.Mem, le_iSup
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
let : motive x
⊢ motive x

Tactic:
let T : Subalgebra R A :=
  { carrier := {x | motive x}
    mul_mem' {a b} := mul a b
    add_mem' {a b} := add a b
    algebraMap_mem' := algebraMap }
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
T : Subalgebra R A :=
  { carrier := {x : A | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
suffices : iSup S ≤ T
⊢ motive x

Tactic:
suffices iSup S ≤ T from this mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
T : Subalgebra R A :=
  { carrier := {x : A | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
rwa rwa₁ rwa₂ rwa₃ : ∀ (i : ι), S i ≤ T
⊢ iSup S ≤ T

Tactic:
rwa [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
⊢ motive x mem

Tactic:
Exists.elim ?_ fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) ↦ hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
refine : ∃ (x_1 : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x), motive x x_1
⊢ motive x mem

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) ↦ hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
⊢ ∃ (x_1 : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x), motive x x_1

Tactic:
iSup_induction S (motive := fun x' ↦ ∃ h, motive x' h) mem
    (fun _ _ h ↦ ⟨_, basic _ _ h⟩) (fun _ _ h h' ↦ ⟨_, add _ _ _ _ h.2 h'.2⟩)
    (fun _ _ h h' ↦ ⟨_, mul _ _ _ _ h.2 h'.2⟩) fun _ ↦ ⟨_, algebraMap _⟩

Premises used: iSup, Exists.intro, Algebra.mem_iSup_of_mem, Algebra.iSup_induction, AddMemClass.add_mem, Subalgebra.algebraMap_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x → Prop
x : A
mem : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) y), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
⊢ ∃ (x_1 : Membership.mem (γ := Subalgebra R A) (⨆ (i : ι), S i) x), motive x x_1

Tactic:
exact iSup_induction S (motive := fun x' ↦ ∃ h, motive x' h) mem
    (fun _ _ h ↦ ⟨_, basic _ _ h⟩) (fun _ _ h h' ↦ ⟨_, add _ _ _ _ h.2 h'.2⟩)
    (fun _ _ h h' ↦ ⟨_, mul _ _ _ _ h.2 h'.2⟩) fun _ ↦ ⟨_, algebraMap _⟩

Premises used: iSup, Exists.intro, Algebra.mem_iSup_of_mem, Algebra.iSup_induction, AddMemClass.add_mem, Subalgebra.algebraMap_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ Membership.mem (γ := Subalgebra R A) ⊥ x ↔
    Membership.mem (γ := Set A) (Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)) x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{v + 1} (α := Submodule R A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A)
    (1 : Submodule R A)

Tactic:
Submodule.one_eq_range.symm

Premises used: setOf, LinearMap.range, Set.range, Eq.symm, Submodule.one_eq_range, Submodule.copy
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ (↑⊥ : Set A) = Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
A : Type u_1
inst : CommRing A
R : Subring A
⊢ Subalgebra.toSubring (R := ↥R) ⊥ = R

Tactic:
aesop (add norm Subalgebra.mem_carrier.symm)

Premises used: Subalgebra.mem_carrier, Iff.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
rw : Membership.mem (γ := Subalgebra R A) ⊤ x
⊢ x ∈ S

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := Subalgebra R A) ⊤ x

Tactic:
mem_top

Premises used: Algebra.mem_top
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := Subalgebra R A) ⊤ x

Tactic:
exact mem_top

Premises used: Algebra.mem_top
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := Subalgebra R A) ⊤ x
⊢ S = ⊤

Tactic:
ext x
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := Subalgebra R A) ⊤ x

Tactic:
⟨fun _ => mem_top, fun _ => h x⟩

Premises used: Algebra.mem_top, Iff.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := Subalgebra R A) ⊤ x

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ f.range = ⊤ ↔ Function.Surjective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
Algebra.eq_top_iff

Premises used: Set.Mem, setOf, Algebra.eq_top_iff, Set.range, Function.Surjective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra R A) (AlgHom.range (ofId R A)) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra R A) (AlgHom.range (AlgHom.id R A)) ⊤

Tactic:
SetLike.coe_injective Set.range_id

Premises used: SetLike.coe_injective, Set.range_id
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Subalgebra.map f ⊤ = f.range

Tactic:
SetLike.coe_injective Set.image_univ

Premises used: Set.image_univ, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) (Subalgebra.map f ⊥) : Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) ⊥ : Submodule R B)

Tactic:
simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _

Premises used: Algebra.toSubmodule_bot, Subalgebra.map_toSubmodule, Submodule.map_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Subalgebra.comap f ⊤ = ⊤

Tactic:
eq_top_iff.2 fun _x => mem_top

Premises used: Iff.mpr, Algebra.mem_top, Algebra.eq_top_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Function.Surjective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ↔
    Eq.{v + 1} (α := Subalgebra R A) ⊤ ⊥

Tactic:
⟨fun h =>
    eq_bot_iff.2 fun y _ =>
      let ⟨_x, hx⟩ := h y
      hx ▸ Subalgebra.algebraMap_mem _ _,
    fun h y => Algebra.mem_bot.1 <| eq_bot_iff.1 h (Algebra.mem_top : y ∈ _)⟩

Premises used: _private.0.Algebra.surjective_algebraMap_iff.match_1, Iff.mpr, Algebra.mem_top, Algebra.mem_bot, Membership.mem, Eq.rec, Bot.bot, Iff.intro, Iff.mp, Subalgebra.algebraMap_mem, eq_bot_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : Semiring A
inst_2 : Nontrivial A
inst_3 : Algebra R A
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ↔
    Eq.{u_2 + 1} (α := Subalgebra R A) ⊤ ⊥

Tactic:
⟨fun h => surjective_algebraMap_iff.1 h.2, fun h =>
    ⟨(algebraMap R A).injective, surjective_algebraMap_iff.2 h⟩⟩

Premises used: Iff.mpr, Algebra.algebraMap, RingHom.injective, And.right, Algebra.surjective_algebraMap_iff, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
inst_5 : Subsingleton.{v + 1} (Subalgebra R A)
⊢ Subsingleton (A →ₐ[R] B)

Tactic:
⟨fun f g =>
    AlgHom.ext fun a =>
      have : a ∈ (⊥ : Subalgebra R A) := Subsingleton.elim (⊤ : Subalgebra R A) ⊥ ▸ mem_top
      let ⟨_x, hx⟩ := Set.mem_range.mp (mem_bot.mp this)
      hx ▸ (f.commutes _).trans (g.commutes _).symm⟩

Premises used: _private.0.Algebra.surjective_algebraMap_iff.match_1, Algebra.mem_top, Set.mem_range, Algebra.mem_bot, Eq.rec, Bot.bot, AlgHom.ext, Subsingleton.intro, AlgHom.commutes, Iff.mp, Subsingleton.elim, Top.top, Eq.symm, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
inst_5 : Subsingleton.{v + 1} (Subalgebra R A)
⊢ Subsingleton (A ≃ₐ[R] B)

Tactic:
⟨fun f g => AlgEquiv.ext fun x => AlgHom.ext_iff.mp (Subsingleton.elim f.toAlgHom g.toAlgHom) x⟩

Premises used: AlgEquiv.toAlgHom, AlgHom.ext_iff, Subsingleton.intro, AlgEquiv.ext, Iff.mp, Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
inst_5 : Subsingleton.{w + 1} (Subalgebra R B)
f g : A ≃ₐ[R] B
rw : f.symm.symm = g
rw₁ : g.symm.symm = g
rw₂ rw₃ : g = g
⊢ f = g

Tactic:
rw [← f.symm_symm, Subsingleton.elim f.symm g.symm, g.symm_symm]

Premises used: AlgEquiv.symm, Subsingleton.elim, AlgEquiv.symm_symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 : Subalgebra R A
S : Subalgebra R R
⊢ S = default

Tactic:
le_antisymm ?_ bot_le

Premises used: le_antisymm, bot_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 : Subalgebra R A
S : Subalgebra R R
refine : S ≤ default
⊢ S = default

Tactic:
refine le_antisymm ?_ bot_le

Premises used: le_antisymm, bot_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 : Subalgebra R A
S : Subalgebra R R
x : R
_ : x ∈ S → Membership.mem (γ := Subalgebra R R) default x
⊢ x ∈ S → Membership.mem (γ := Subalgebra R R) default x

Tactic:
_
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 : Subalgebra R A
S : Subalgebra R R
x : R
h : x ∈ S
⊢ Membership.mem (γ := Subalgebra R R) default x

Tactic:
simp only [Set.mem_range, mem_bot, algebraMap_self_apply, exists_apply_eq_apply, default]

Premises used: Algebra.algebraMap_self_apply, Inhabited.default, Set.mem_range, Algebra.mem_bot, exists_apply_eq_apply
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra R A) (center R A) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ A)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subalgebra R A) (centralizer R s) ⊤ ↔ s ⊆ (↑(center R A) : Set A)

Tactic:
SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

Premises used: Set.centralizer_eq_top_iff_subset, SetLike.ext'_iff, Iff.trans
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
⊢ Eq (α := Subalgebra R A) (equalizer φ ψ) ⊤ ↔ φ = ψ

Tactic:
simp [SetLike.ext_iff, DFunLike.ext_iff]

Premises used: SetLike.ext_iff, DFunLike.ext_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ : F
⊢ Eq (α := Subalgebra R A) (equalizer φ φ) ⊤

Tactic:
equalizer_eq_top.2 rfl

Premises used: Iff.mpr, AlgHom.equalizer_eq_top, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑S : Set A)
hT : Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑T : Set A)
⊢ S ≤ equalizer φ ψ

Tactic:
rw [← le_equalizer] at hS hT ⊢

Premises used: AlgHom.le_equalizer
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑S : Set A)
hT : Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑T : Set A)
hS₁ : S ≤ equalizer φ ψ
⊢ T ≤ equalizer φ ψ

Tactic:
rw [← le_equalizer] at hS hT ⊢

Premises used: AlgHom.le_equalizer