awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S_1 : NonUnitalSubalgebra R A
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
b : B
hb :
  b ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))
rcases :
  ∀ (a : A) (ha : a ∈ (↑S.toNonUnitalSubsemiring : Set A)),
    HSMul.hSMul (β := B) r (((↑f : A →ₙ+* B) : (a : A) → B) a : B) ∈
      AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (NonUnitalSubsemiring.toAddSubmonoid
            (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))
⊢ r • b ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))

Tactic:
rcases hb with ⟨a, ha, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S_1 : NonUnitalSubalgebra R A
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
a : A
ha : a ∈ (↑S.toNonUnitalSubsemiring : Set A)
⊢ HSMul.hSMul (β := B) r (((↑f : A →ₙ+* B) : (a : A) → B) a : B) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))

Tactic:
map_smulₛₗ f r a ▸ Set.mem_image_of_mem f (S.smul_mem' r ha)

Premises used: Set.Mem, Eq.rec, MulActionSemiHomClass.map_smulₛₗ, NonUnitalSubalgebra.smul_mem', Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S_1 : NonUnitalSubalgebra R A
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
a : A
ha : a ∈ (↑S.toNonUnitalSubsemiring : Set A)
⊢ HSMul.hSMul (β := B) r (((↑f : A →ₙ+* B) : (a : A) → B) a : B) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))

Tactic:
exact map_smulₛₗ f r a ▸ Set.mem_image_of_mem f (S.smul_mem' r ha)
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S₁ S₂ : NonUnitalSubalgebra R A
f : F
⊢ S₁ ≤ S₂ → LE.le (α := NonUnitalSubalgebra R B) (map f S₁) (map f S₂)

Tactic:
Set.image_mono

Premises used: Set.Mem, Set.image_mono, setOf, Set.Subset, Set.image
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective (α := NonUnitalSubalgebra R A) (β := NonUnitalSubalgebra R B) (map f)

Tactic:
fun _S₁ _S₂ ih =>
  ext <| Set.ext_iff.1 <| Set.image_injective.2 hf <| Set.ext <| SetLike.ext_iff.mp ih

Premises used: Iff.mpr, Set.ext, Set.image_injective, SetLike.ext_iff, NonUnitalSubalgebra.ext, Iff.mp, Set.ext_iff, Function.Injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ map (F := A →ₙₐ[R] A) (NonUnitalAlgHom.id R A) S = S

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S : NonUnitalSubalgebra R A
g : B →ₙₐ[R] C
f : A →ₙₐ[R] B
⊢ Eq.{w' + 1} (α := NonUnitalSubalgebra R C) (map g (map f S : NonUnitalSubalgebra R B)) (map (g.comp f) S)

Tactic:
SetLike.coe_injective <| Set.image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
f : F
y : B
⊢ Membership.mem (γ := NonUnitalSubalgebra R B) (map f S) y ↔ ∃ x ∈ S, (f : (a : A) → B) x = y

Tactic:
NonUnitalSubsemiring.mem_map

Premises used: Set.Mem, NonUnitalSubsemiring.mem_map
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
f : F
⊢ Eq (α := Submodule R B) (toSubmodule (map f S)) (Submodule.map (LinearMapClass.linearMap f) S.toSubmodule)

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
f : F
⊢ Eq (α := NonUnitalSubsemiring B) (toNonUnitalSubsemiring (map f S))
    (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
f : F
⊢ (↑(map f S) : Set B) = (⇑f : (a : A) → B) '' (↑S : Set A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
f : F
U : NonUnitalSubalgebra R B
⊢ map f S ≤ U ↔ S ≤ comap f U

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
f : F
⊢ GaloisConnection (α := NonUnitalSubalgebra R A) (β := NonUnitalSubalgebra R B) (map f) (comap f)

Tactic:
fun _ _ => map_le

Premises used: NonUnitalSubalgebra.map_le, GaloisConnection
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R B
f : F
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (comap f S) x ↔ Membership.mem (α := B) S ((f : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R B
f : F
⊢ (↑(comap f S) : Set A) = (⇑f : (a : A) → B) ⁻¹' (↑S : Set B)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R_1 : Type u
A_1 : Type v
B : Type w
C : Type w'
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R_1 A_1
inst_5 : Module R_1 B
inst_6 : Module R_1 C
S_1 : NonUnitalSubalgebra R_1 A_1
inst_7 : FunLike F A_1 B
inst_8 : NonUnitalAlgHomClass F R_1 A_1 B
R : Type u_1
A : Type u_2
inst_9 : CommSemiring R
inst_10 : NonUnitalSemiring A
inst_11 : NoZeroDivisors A
inst_12 : Module R A
S : NonUnitalSubalgebra R A
⊢ NoZeroDivisors.{u_2} ↥S

Tactic:
NonUnitalSubsemiringClass.noZeroDivisors S

Premises used: NonUnitalSubsemiringClass.noZeroDivisors
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
p : Submodule R A
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
x : A
⊢ x ∈ p.toNonUnitalSubalgebra h_mul ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
p : Submodule R A
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
⊢ (↑(p.toNonUnitalSubalgebra h_mul) : Set A) = (↑p : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
p : Submodule R A
hmul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
⊢ p.toNonUnitalSubalgebra hmul =
    { carrier := (↑p : Set A), add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }

Tactic:
rfl

Premises used: Submodule.toNonUnitalSubalgebra, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
p : Submodule R A
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
⊢ (p.toNonUnitalSubalgebra h_mul).toSubmodule = p

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ S.toSubmodule.toNonUnitalSubalgebra ⋯ = S

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : A
⊢ HSMul.hSMul (β := B) r (((↑φ : A →ₙ+* B) : (a : A) → B) a : B) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid (NonUnitalRingHom.srange (F := A →ₙ+* B) (↑φ : A →ₙ+* B))))

Tactic:
⟨r • a, map_smul φ r a⟩

Premises used: Set.Mem, setOf, Exists.intro, HSMul.hSMul, Set.range, map_smul
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : A
⊢ HSMul.hSMul (β := B) r (((↑φ : A →ₙ+* B) : (a : A) → B) a : B) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid (NonUnitalRingHom.srange (F := A →ₙ+* B) (↑φ : A →ₙ+* B))))

Tactic:
exact ⟨r • a, map_smul φ r a⟩
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
φ : F
y : B
⊢ Membership.mem (γ := NonUnitalSubalgebra R B) (NonUnitalAlgHom.range φ) y ↔ ∃ (x : A), (φ : (a : A) → B) x = y

Tactic:
NonUnitalRingHom.mem_srange

Premises used: NonUnitalRingHom.mem_srange, Set.Mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
φ : F
x : A
⊢ Membership.mem (α := B) (γ := NonUnitalSubalgebra R B) (NonUnitalAlgHom.range φ) ((φ : (a : A) → B) x : B)

Tactic:
(NonUnitalAlgHom.mem_range φ).2 ⟨x, rfl⟩

Premises used: Iff.mpr, NonUnitalAlgHom.mem_range, Exists.intro, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
φ : F
h :
  ∀ (x : B),
    x ∈ (↑(NonUnitalAlgHom.range φ) : Set B) ↔
      Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
⊢ (↑(NonUnitalAlgHom.range φ) : Set B) = Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
φ : F
x : B
h :
  Membership.mem (γ := NonUnitalSubalgebra R B) (NonUnitalAlgHom.range φ) x ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
h₁ :
  (∃ (x_1 : A), (φ : (a : A) → B) x_1 = x) ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
h₂ h₃ : (∃ (x_1 : A), (φ : (a : A) → B) x_1 = x) ↔ ∃ (y : A), (φ : (a : A) → B) y = x
⊢ x ∈ (↑(NonUnitalAlgHom.range φ) : Set B) ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x

Tactic:
rw [SetLike.mem_coe, mem_range, Set.mem_range]

Premises used: Set.mem_range, NonUnitalAlgHom.mem_range, SetLike.mem_coe
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
f : A →ₙₐ[R] B
g : B →ₙₐ[R] C
⊢ Eq.{w' + 1} (α := NonUnitalSubalgebra R C) (NonUnitalAlgHom.range (g.comp f))
    (NonUnitalSubalgebra.map g (NonUnitalAlgHom.range f : NonUnitalSubalgebra R B))

Tactic:
SetLike.coe_injective (Set.range_comp g f)

Premises used: Set.range_comp, SetLike.coe_injective, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
f : A →ₙₐ[R] B
g : B →ₙₐ[R] C
⊢ LE.le.{w'} (α := NonUnitalSubalgebra R C) (NonUnitalAlgHom.range (g.comp f)) (NonUnitalAlgHom.range g)

Tactic:
SetLike.coe_mono (Set.range_comp_subset_range f g)

Premises used: Set.range_comp_subset_range, Set.Subset, DFunLike.coe, SetLike.coe_mono
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
f : F
S : NonUnitalSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ Eq (α := A →ₙₐ[R] B) (comp (NonUnitalSubalgebraClass.subtype S) (codRestrict f S hf))
    (NonUnitalAlgHomClass.toNonUnitalAlgHom f)

Tactic:
rfl

Premises used: rfl, NonUnitalAlgHomClass.toNonUnitalAlgHom
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
f : F
S : NonUnitalSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
x : A
⊢ Eq.{w + 1} (α := B)
    ((↑(((codRestrict f S hf : NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) A ↥S) : (a : A) → ↥S) x) : B) : B)
    ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
f : F
S : NonUnitalSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ Function.Injective.{v + 1, w + 1} (α := A) (β := ↥S) (⇑(codRestrict f S hf) : (a : A) → ↥S) ↔
    Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
⟨fun H _x _y hxy => H <| Subtype.ext hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩

Premises used: congr_arg, Iff.intro, Subtype.val, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 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)
rw₄ 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.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x + y)

Tactic:
rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]

Premises used: map_add, Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) 0 : B) ((ψ : (a : A) → B) 0 : B)
rw₁ : Eq.{w + 1} (α := B) (0 : B) ((ψ : (a : A) → B) 0 : B)
rw₂ rw₃ : Eq.{w + 1} (α := B) 0 0
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} 0

Tactic:
rw [Set.mem_setOf_eq, map_zero, map_zero]

Premises used: map_zero, Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 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)
rw₄ 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.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x * y)

Tactic:
rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]

Premises used: Set.mem_setOf_eq, map_mul
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : 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 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (r • x) : B) ((ψ : (a : A) → B) (r • x) : B)
rw₁ : HSMul.hSMul (β := B) r ((ϕ : (a : A) → B) x : B) = (ψ : (a : A) → B) (r • x)
rw₂ : HSMul.hSMul (β := B) r ((ϕ : (a : A) → B) x : B) = HSMul.hSMul (β := B) r ((ψ : (a : A) → B) x : B)
rw₃ rw₄ : HSMul.hSMul (β := B) r ((ψ : (a : A) → B) x : B) = HSMul.hSMul (β := B) r ((ψ : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (r • x)

Tactic:
rw [Set.mem_setOf_eq, map_smul, map_smul, hx]

Premises used: Set.mem_setOf_eq, map_smul
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
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
φ ψ : F
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (equalizer φ ψ) x ↔
    Eq.{w + 1} (α := B) ((φ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf