mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Aut

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
f : R ≃+* R
⊢ ⇑(f ^ 0) = (⇑f)^[0]

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
n : ℕ
s : Set R
⊢ closure {↑n} ⊔ closure s = closure s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
n : ℕ
s : Set R
⊢ closure (insert (↑n) s) = closure s

Tactic:
rw [Set.insert_eq, closure_union]
  simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ ↑f.rangeS = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_rangeS,

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Algebra.Ring.Action.Group

Goal state before:
pp: G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
x✝ : R
⊢ (let __src := DistribMulAction.toAddEquiv R 1;
      let __src_1 := toRingHom G R 1;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝ =
    1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ Subring.map f ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
s : Set (Subring R)
⊢ ↑(⨅ t ∈ s, t.toSubmonoid) = ⋂ t ∈ s, ↑t

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
s : Set (Subring R)
⊢ ↑(⨅ t ∈ s, t.toAddSubgroup) = ⋂ t ∈ s, ↑t

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.zero_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝ x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ 0 * x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.zero_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝ x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
L : List (List R)
hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
⊢ (List.map List.prod (List.map (List.cons (-1)) [])).sum = -(List.map List.prod []).sum

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
n : ℤ
s : Set R
⊢ closure {↑n} ⊔ closure s = closure s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
n : ℤ
s : Set R
⊢ closure (insert (↑n) s) = closure s

Tactic:
rw [Set.insert_eq, closure_union]
  simp

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
x✝ : 0 ≠ 1
⊢ ¬Irreducible (x ^ 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f a * f b = f (a * b)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
a : M
⊢ e.symm (e a) = a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
h : Prime p
a : N
⊢ e (e.symm a) = a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
⊢ x * ↑1 = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ 1 ∈ {x | ∀ (y : M₀), x * y = 0 → y = 0}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ 1 ∈ {x | ∀ (y : M₀), y * x = 0 → y = 0}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x ↔ IsUnit y ∨ x ~ᵤ y

Tactic:
by
  constructor
  · rintro ⟨z, hz⟩
    obtain (h | h) := hx.isUnit_or_isUnit hz
    · exact Or.inl h
    · rw [hz]
      exact Or.inr (associated_mul_unit_left _ _ h)
  · rintro (hy | h)
    · exact hy.dvd
    · exact h.symm.dvd

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ p = p * ↑u * ↑u⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsRight M₀ = M₀⁰

Tactic:
by
  rw [← nonZeroDivisorsLeft_eq_right, nonZeroDivisorsLeft_eq_nonZeroDivisors]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a' : Associates M
a : M
⊢ ⟦1 * a⟧ = ⟦a⟧

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a' : Associates M
a : M
⊢ ⟦a * 1⟧ = ⟦a⟧

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
x : G₀
u : G₀ˣ
⊢ (fun u ↦ Units.mk0 ↑u ⋯) ((fun u ↦ ⟨↑u, ⋯⟩) u) = u

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
x : G₀
u v : ↥G₀⁰
⊢ Units.mk0 ↑(u * v) ⋯ = Units.mk0 ↑u ⋯ * Units.mk0 ↑v ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type ?u.3
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ ⟨↑u, ⋯⟩ * ⟨↑u⁻¹, ⋯⟩ = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type ?u.3
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ ⟨↑u⁻¹, ⋯⟩ * ⟨↑u, ⋯⟩ = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsPrimal (Associates.mk a) ↔ IsPrimal a

Tactic:
IsPrimal,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ ⦃b c : Associates M⦄, Associates.mk a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ Associates.mk a = a₁ * a₂) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : x ∈ comap f (map f s)
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
rw [mem_comap, mem_map] at hx

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, f x_1 = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
u : (Associates M)ˣ
⊢ a * ↑u ∣ a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
x✝ : M₂
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ DvdNotUnit q r

Tactic:
refine ⟨hq, x * u, mt isUnit_of_mul_isUnit_left hx.1, ?_⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ r = q * (x * ↑u)
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
K : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
x✝ : M₂
⊢ x✝ ∈ (f.domRestrict K).range ↔ x✝ ∈ map f K

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
hp : Prime p
n : ℕ
⊢ q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i

Tactic:
by
  induction n generalizing q with
  | zero =>
    simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
  | succ n ih =>
    refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
    rw [pow_succ'] at h
    rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
    · rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
      rcases h with ⟨i, hi, hq⟩
      refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
      rw [pow_succ']
    · obtain ⟨i, hi, hq⟩ := ih.mp hno
      exact ⟨i, hi.trans n.le_succ, hq⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: case e_a
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
r : R
⊢ (algebraMap R A₂) r = e.toRingEquiv ((algebraMap R A₁) r)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
x✝ : α
⊢ x✝ ∈ 0⁻¹ ↔ x✝ ∈ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x✝ : A₂
⊢ ((↑e).comp ↑e.symm) x✝ = (AlgHom.id R A₂) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x✝ : A₁
⊢ ((↑e.symm).comp ↑e) x✝ = (AlgHom.id R A₁) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a✝ : A₁
⊢ (e.trans e.symm) a✝ = refl a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a✝ : A₂
⊢ (e.symm.trans e) a✝ = refl a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
t : Set β
a x✝ : α
⊢ {x✝ • 0} = 0

Tactic:
by rw [smul_zero, singleton_zero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
⊢ s = 0 ∨ t = 0

Tactic:
by
    by_contra! H
    have hst : (s * t).Nonempty := h.symm.subst zero_nonempty
    rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H
    simp only [not_subset, mem_zero] at H
    obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
    exact (eq_zero_or_eq_zero_of_mul_eq_zero <| h.subset <| mul_mem_mul hs ht).elim ha hb

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ((e₁.arrowCongr e₃) (g.comp f)) x✝ = (((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulLeft R x)) x✝ = (LinearMap.mulLeft R (f x)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulRight R x)) x✝ = (LinearMap.mulRight R (f x)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: case mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
fst✝ snd✝ : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulLeftRight R (fst✝, snd✝))) x✝ = (LinearMap.mulLeftRight R (Prod.map ⇑f ⇑f (fst✝, snd✝))) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n : ℕ
x✝ : A₁
⊢ (e ^ Nat.zero) x✝ = (⇑e)^[Nat.zero] x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Semiring T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
f : S →ₐ[R] T
x✝ : ULift.{u₂, u_1} R
⊢ (↑↑((↑ULift.algEquiv.{u_1, u_3, u₃}.symm).comp (f.comp ↑ULift.algEquiv.{u_1, u_2, u₁})).toRingHom).toFun
      ((algebraMap (ULift.{u₂, u_1} R) (ULift.{u₁, u_2} S)) x✝) =
    (algebraMap (ULift.{u₂, u_1} R) (ULift.{u₃, u_3} T)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝¹ : R
x✝ : M₂
⊢ (restrictScalars R e) (((algebraMap R (Module.End S M₁)) x✝¹) (↑e.symm x✝)) =
    ((algebraMap R (Module.End S M₂)) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ map p.subtype ⊤ = p

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ i.range
x✝ : M₁
⊢ (i ∘ₗ f.codRestrictOfInjective i hi hf) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
p : Submodule R M
x✝ : M
⊢ x✝ ∈ -restrictScalars S p ↔ x✝ ∈ restrictScalars S (-p)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ {r} • N
⊢ r • m₁ + r • m₂ = r • (m₁ + m₂)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ 0 = r • 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x✝ : α
⊢ c x✝ = (ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ⊥ ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ b ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ 0 ∈ p'

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ y + 0 = y

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ 0 ∈ p

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ 0 + y = y

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ 0 ∈ p

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ 0 ∈ p' ∧ 0 + 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
z : M
⊢ (∃ y ∈ p, ∃ z_1 ∈ p', y + z_1 = z) ↔ ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x✝) ↔ ∃ x ∈ ↑p, ∃ y ∈ ↑p', x + y = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure ∅ = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
a : α
⊢ supClosure {a} = {a}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure Set.univ = Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsAtom ⟨b, h⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsCoatom ⟨a, h⟩

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ 1 • y = y

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ 0 • y = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : M
a : R
⊢ y ∈ {y}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ y = yᶜᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : x = y
⊢ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ x)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure ∅ = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
a : α
⊢ latticeClosure {a} = {a}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure Set.univ = Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a ≤ b ∧ b ≤ a

Tactic:
le_iff_atom_le_imp,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ b ≤ a
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ R ∙ x = ⊥ ↔ x = 0

Tactic:
simp

Goal state after: