awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a : M
ha : ¬IsUnit a
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hr_1 : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
hr : r = a * 1
hb : ¬IsUnit.{u_1} (M := M) 1
hn : 1 = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
⊢ False

Tactic:
simp at hb
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
N : ℕ
hr : m r + n r = N.succ.succ
⊢ False

Tactic:
simp [hr, hr₀, pow_add, mul_assoc, mul_left_comm] at hr'

Premises used: mul_assoc, pow_add, mul_left_comm
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
⊢ False

Tactic:
match hr : m r + n r with
  -- If that power is `0`, then `r` can be written as a product of elements of `S \ {r}` and `S` was
  -- not minimal. Contradiction.
  | 0 =>
    have : ({r} : Set M) ⊆ closure (S \ {r}) := by
      simp only [hr, pow_zero, one_mul] at hr'
      rw [hr', Set.singleton_subset_iff]
      refine mul_mem ?_ ?_ <;> refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _ <;>
        rw [← hr'] <;> simpa using hs
    specialize hSmax (y := S \ {r}) (by simp [Submonoid.closure_sdiff_eq_closure this, hSgen])
      Finset.sdiff_subset
    simpa using hSmax hrS
  -- Assume that power is `1`.
  | 1 =>
    -- By cancelling on both sides we get `∏ s ∈ S \ {r}, s ^ (m s + n s) = 1`.
    simp only [hr, pow_one, mul_assoc, eq_comm (a := r), mul_eq_left, LeftCancelMonoid.mul_eq_one,
      Finset.prod_eq_one_iff] at hr'
    -- Since `M` has a single unit, this means that
    -- `∏ s ∈ S \ {r}, s ^ m s = ∏ s ∈ S \ {r}, s ^ n s = 1`.
    -- Furthermore, `m r + n r = 1` implies that one of `m r` or `n r` is zero.
    -- Therefore one of `a` or `b` is `1`, contradicting the fact that they are non-units.
    obtain h | h : m r = 0 ∨ n r = 0 := by lia
    · obtain rfl : a = 1 := by simpa [h, Finset.prod_eq_one hr'.1] using hm
      simp at ha
    · obtain rfl : b = 1 := by simpa [h, Finset.prod_eq_one hr'.2] using hn
      simp at hb
  -- If that power is at least `2`, then we can write `1` as `r` times something.
  -- Since `M` has a single unit, this means that `r = 1`. Contradiction.
  | N + 2 => simp [hr, hr₀, pow_add, mul_assoc, mul_left_comm] at hr'
-- Module: Mathlib.Algebra.AffineMonoid.UniqueSums
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
inst_1 : AddMonoid.FG M
inst_2 : IsAddTorsionFree M
⊢ TwoUniqueSums M

Tactic:
.of_injective_addHom (embedding M).toAddHom embedding_injective inferInstance

Premises used: AddMonoidHom.toAddHom, inferInstance, TwoUniqueSums.of_injective_addHom, AffineAddMonoid.embedding, AffineAddMonoid.embedding_injective
-- Module: Mathlib.Algebra.AffineMonoid.UniqueSums
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Monoid.FG M
inst_2 : IsMulTorsionFree M
⊢ TwoUniqueProds M

Tactic:
Multiplicative.instTwoUniqueProdsOfTwoUniqueSums (M := Additive M)

Premises used: Additive, Multiplicative.instTwoUniqueProdsOfTwoUniqueSums, Multiplicative
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
r : R
⊢ (algebraMap R PUnit.{u_4 + 1} : (a : R) → PUnit.{u_4 + 1}) r = PUnit.unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq (α := ULift.{u_4, u_2} A)
    ((algebraMap R (ULift.{u_4, u_2} A) : (a : R) → ULift.{u_4, u_2} A) r : ULift.{u_4, u_2} A)
    ({ down := (algebraMap R A : (a : R) → A) r } : ULift.{u_4, u_2} A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{u_2 + 1} (α := A)
    (ULift.down.{u_4, u_2} ((algebraMap R (ULift.{u_4, u_2} A) : (a : R) → ULift.{u_4, u_2} A) r) : A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : ULift.{u_4, u_1} R
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap (ULift.{u_4, u_1} R) A : (a : ULift.{u_4, u_1} R) → A) r : A)
    ((algebraMap R A : (a : R) → A) r.down : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Subsemiring R
⊢ algebraMap (↥S) R = S.subtype

Tactic:
rfl

Premises used: Subsemiring.subtype, rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
C : Type u_4
inst_1 : SetLike C R
inst_2 : SubsemiringClass C R
S : C
⊢ Eq (α := (a : ↥S) → R) (⇑(algebraMap (↥S) R) : (a : ↥S) → R) (Subtype.val (p := fun (x : R) ↦ x ∈ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
C : Type u_4
inst_1 : SetLike C R
inst_2 : SubsemiringClass C R
S : C
x : ↥S
⊢ (algebraMap (↥S) R : (a : ↥S) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_5
inst : CommRing R
S : Subring R
⊢ algebraMap (↥S) R = S.subtype

Tactic:
rfl

Premises used: Subring.subtype, rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_5
inst : CommRing R
S : Subring R
⊢ Eq (α := (a : ↥S) → R) (⇑(algebraMap (↥S) R) : (a : ↥S) → R) (Subtype.val (p := fun (x : R) ↦ x ∈ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_5
inst : CommRing R
S : Subring R
x : ↥S
⊢ (algebraMap (↥S) R : (a : ↥S) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submonoid R
x : ↥M
⊢ Membership.mem (α := S) (γ := Submonoid S) (algebraMapSubmonoid S M) ((algebraMap R S : (a : R) → S) (↑x : R) : S)

Tactic:
Set.mem_image_of_mem (algebraMap R S) x.2

Premises used: Algebra.algebraMap, Set.Mem, setOf, Set.mem_image_of_mem, Set.image, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
⊢ algebraMapSubmonoid R M = M

Tactic:
Submonoid.map_id M

Premises used: Submonoid.map_id, Submonoid.map, Algebra.algebraMapSubmonoid
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Algebra R S
r : R
⊢ Eq (α := Submonoid S) (algebraMapSubmonoid S (Submonoid.powers r))
    (Submonoid.powers ((algebraMap R S : (a : R) → S) r))

Tactic:
simp [Algebra.algebraMapSubmonoid]

Premises used: Algebra.algebraMapSubmonoid
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Algebra R S
y : R
hy : y ∈ (↑(IsUnit.submonoid R) : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S) (IsUnit.submonoid S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
hy.map _

Premises used: Set.Mem, setOf, IsUnit, IsUnit.map
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Algebra R S
y : R
hy : y ∈ (↑(IsUnit.submonoid R) : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S) (IsUnit.submonoid S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
exact hy.map _

Premises used: IsUnit.map
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
rw :
  x * x - HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
rw₁ :
  x * x - HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
rw₂ rw₃ :
  x * x - HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x =
    x * x - HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x

Tactic:
rw [mul_sub, ← commutes, sub_mul]

Premises used: mul_sub, sub_mul, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
⊢ x * HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 =
    HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 * x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
ih :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
succ :
  x *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₁ :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₂ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₃ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      (x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₄ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₅ succ₆ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x

Tactic:
rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

Premises used: mul_assoc, Algebra.mul_sub_algebraMap_commutes, pow_succ'
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
zero :
  x * HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 =
    HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 * x
succ :
  ∀ (n : ℕ)
    (ih :
      x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x),
    x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

Premises used: mul_assoc, Algebra.mul_sub_algebraMap_commutes, pow_succ'
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R_1 : Type u_1
A : Type u_2
M : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
z : ℕ
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) (↑(↑z : ℤ) : R) : A) ((↑z : A) : A)

Tactic:
simp only [Int.cast_natCast, map_natCast]

Premises used: Int.cast_natCast, map_natCast
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R_1 : Type u_1
A : Type u_2
M : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
z : ℕ
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) (↑(Int.negSucc z) : R) : A) (-(↑(z + 1) : A) : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
a : R
⊢ (algebraMap R (End S M) : (a : R) → End S M) a = HSMul.hSMul (β := M →ₗ[S] M) a LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
a : R
m : M
⊢ (((algebraMap R (End S M) : (a : R) → End S M) a : End S M) : (a : M) → M) m = a • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
K : Type u
V : Type v
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
a : K
ha : a ≠ 0
⊢ Eq.{v + 1} (α := Submodule K V)
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((algebraMap K (End K V) : (a : K) → End K V) a)) ⊥

Tactic:
LinearMap.ker_smul _ _ ha

Premises used: Set.Mem, LinearMap.ker, setOf, Submodule.comap, Set.preimage, Set.singleton, LinearMap.ker_smul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
⊢ Injective (α := M) (β := M) (⇑(↑h.unit : End S M) : (a : M) → M)

Tactic:
((isUnit_iff _).mp h).injective

Premises used: Module.End.isUnit_iff, Function.Bijective.injective, Iff.mp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
apply_fun :
  Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)
    (((↑h.unit : End S M) : (a : M) → M) m' : M)
⊢ ((↑h.unit⁻¹ : End S M) : (a : M) → M) m = m'

Tactic:
apply_fun ⇑h.unit.val using ((isUnit_iff _).mp h).injective

Premises used: Units.val, Module.End.isUnit_iff, Function.Bijective.injective, Iff.mp, IsUnit.unit
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
rw :
  Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) (x • m') : M) : M)
    (((↑h.unit : End S M) : (a : M) → M) m' : M)
⊢ Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)
    (((↑h.unit : End S M) : (a : M) → M) m' : M)

Tactic:
rw [H]
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
⊢ Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) (x • m') : M) : M)
    (((↑h.unit : End S M) : (a : M) → M) m' : M)

Tactic:
simpa using Module.End.isUnit_apply_inv_apply_of_isUnit h (x • m')

Premises used: HSMul.hSMul, Module.End.isUnit_apply_inv_apply_of_isUnit
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
apply_fun :
  Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) m' : M)
    (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)
⊢ m' = ((↑h.unit⁻¹ : End S M) : (a : M) → M) m

Tactic:
apply_fun (↑h.unit : M → M) using ((isUnit_iff _).mp h).injective

Premises used: Units.val, Module.End.isUnit_iff, Function.Bijective.injective, Iff.mp, IsUnit.unit, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
rw :
  Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) m' : M)
    (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) (x • m') : M) : M)
⊢ Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) m' : M)
    (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)

Tactic:
rw [H]
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
⊢ Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) m' : M)
    (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) (x • m') : M) : M)

Tactic:
simpa using isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm

Premises used: HSMul.hSMul, Module.End.isUnit_apply_inv_apply_of_isUnit, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
rw :
  (f : (a : A) → B) (r • a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
rw₁ : (f : (a : A) → B) (r • a) = HSMul.hSMul (β := B) r ((f : (a : A) → B) a : B)
rw₂ rw₃ : HSMul.hSMul (β := B) r ((f : (a : A) → B) a : B) = HSMul.hSMul (β := B) r ((f : (a : A) → B) a : B)
⊢ (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)

Tactic:
rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]

Premises used: Algebra.smul_def, map_smul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
rw :
  (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)
rw₁ :
  (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
rw₂ rw₃ :
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
⊢ (f : (a : A) → B) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)

Tactic:
rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]

Premises used: LinearMap.map_algebraMap_mul, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : Semiring R
P Q : Algebra ℕ R
h : ∀ (r : ℕ), Eq (α := R) ((algebraMap ℕ R : (a : ℕ) → R) r : R) ((algebraMap ℕ R : (a : ℕ) → R) r : R)
⊢ P = Q

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : Semiring R
P Q : Algebra ℕ R
r : ℕ
⊢ Eq (α := R) ((algebraMap ℕ R : (a : ℕ) → R) r : R) ((algebraMap ℕ R : (a : ℕ) → R) r : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h :
  ∀ (x : ℕ),
    Eq.{u_3 + 1} (α := A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Nat.cast x) (↑x : A)
⊢ Eq.{u_3 + 1} (α := ℕ → A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Nat.cast) Nat.cast

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : ℕ
⊢ Eq.{u_3 + 1} (α := A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Nat.cast x) (↑x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ Eq (α := ℤ →+* R) (algebraMap ℤ R) (Int.castRingHom R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ Subsingleton.{max (u_1 + 1) 1} (Algebra ℤ R)

Tactic:
⟨fun P Q => Algebra.algebra_ext P Q <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

Premises used: Algebra.algebraMap, RingHom.congr_fun, Int, Subsingleton.intro, Algebra.algebra_ext, Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h :
  ∀ (x : ℤ),
    Eq.{u_3 + 1} (α := A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Int.cast x) (↑x : A)
⊢ Eq.{u_3 + 1} (α := ℤ → A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Int.cast) Int.cast

Tactic:
ext