mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)

Tactic:
rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
n : N
⊢ j n = k n

Tactic:
obtain ⟨⟨m, s⟩, hn : n * f s = f m⟩ := f.surj n

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
⊢ j n = k n
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
⊢ j n = k n

Tactic:
replace h (a) : j (f a) = k (f a) := congr($h a)

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j n = k n
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
⊢ ((monoidOf S).mk' a b).liftOn f H = f a b

Tactic:
by rw [← mk_eq_monoidOf_mk', liftOn_mk]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ (if b = 0 then 0 else ⊤) = ⊤

Tactic:
if_neg hb

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ ⊤ = ⊤
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)

Tactic:
rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inr.coe.coe.top
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a : α
ha : ¬a = 0
b : α
hb : ¬b = 0
hc : ⊤ ≠ 0
⊢ ↑a * ↑b * ⊤ = ⊤

Tactic:
simp [ha, hb]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)

Tactic:
oreDiv_mul_char r₁ r₂ s₁ s₂ r₁ s₂ (by simp [mul_comm]),

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ * r₂ /ₒ (s₂ * s₁) = r₁ * r₂ /ₒ (s₁ * s₂)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : b ≠ 0
⊢ (if b = 0 then 0 else ⊥) = ⊥

Tactic:
if_neg hb

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : b ≠ 0
⊢ ⊥ = ⊥
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) ↔ a ≤ b

Tactic:
by
  refine ⟨?_, exists_succ_iterate_of_le⟩
  rintro ⟨n, rfl⟩
  exact id_le_iterate_of_id_le le_succ n a

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝ : ℕ
p : α → Prop
n m : ℕ
l₁ : List α
h₁ : l₁.length = n
l₂ : List α
h₂ : l₂.length = m
⊢ (l₁ ++ l₂).length = n + m

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β
l : List α
h : l.length = n
⊢ (List.map f l).length = n

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β → φ
x : List α
property✝¹ : x.length = n
y : List β
property✝ : y.length = n
⊢ (zipWith f x y).length = n

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.drop i l).length = n - i

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.take i l).length = min i n

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
rw [Finset.prod_eq_mul_prod_sdiff_singleton_of_mem ha]
    exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: case h
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ofNat α v₁ :: a ∈ decodeList v.succ ∧ encodeList (ofNat α v₁ :: a) = v.succ

Tactic:
simp [decodeList, e, h₂, h₁, encodeList, pair_eq_of_unpair_eq e]

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
⊢ {t | t.Finite ∧ t ⊆ s}.Countable

Tactic:
refine (countable_range fun t : Finset s => Subtype.val '' (t : Set s)).mono ?_

Goal state after:
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
⊢ {t | t.Finite ∧ t ⊆ s} ⊆ range fun t ↦ Subtype.val '' ↑t
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: n : ℕ
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = cons <$> f x <*> Vector.traverse f xs

Tactic:
rintro ⟨xs, rfl⟩; rfl

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ c✝ : α
hab : a✝ ≤ c✝
hba : ¬inl c✝ ≤ inl a✝
⊢ inl a✝ < inl c✝

pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b✝ d✝ : β
hab : b✝ ≤ d✝
hba : ¬inr d✝ ≤ inr b✝
⊢ inr b✝ < inr d✝

Tactic:
· exact LiftRel.inl (hab.lt_of_not_ge fun h => hba <| LiftRel.inl h)

Goal state after:
case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b✝ d✝ : β
hab : b✝ ≤ d✝
hba : ¬inr d✝ ≤ inr b✝
⊢ inr b✝ < inr d✝
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk
ι : Type u
f : ι → Cardinal.{v}
α : Type v
⊢ lift.{u, v} #α ^ sum f = prod fun i ↦ #α ^ f i

Tactic:
| _ α =>

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
c : α
h : f c < f a
hc : f c = b
⊢ c < a

Tactic:
f.lt_iff_lt

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
c : α
h : c < a
hc : f c = b
⊢ c < a
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x✝² : α
x✝¹ x✝ : Part α
ho : x✝¹.Dom
h✝¹ : x✝¹.get ho = x✝²
hp : x✝.Dom
h✝ : x✝.get hp = x✝²
⊢ ∀ (h₁ : x✝¹.Dom) (h₂ : x✝.Dom), x✝¹.get h₁ = x✝.get h₂

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
o : Part α
⊢ ¬o = none → ∃ x, o = some x

Tactic:
eq_none_iff',

Goal state after:
case mp
α : Type u_1
o : Part α
⊢ ¬¬o.Dom → ∃ x, o = some x
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : Part α
⊢ ∀ (a : β), (a ∈ x.bind fun y ↦ some (f y)) ↔ a ∈ map f x

Tactic:
simp [eq_comm]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
⊢ a ∈ x → f a ≤ y

Tactic:
h'

Goal state after:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
⊢ f a ≤ y
Module: Mathlib.Data.Part

Goal state before:
pp: case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
⊢ b ∈ x >>= f → b ∈ y

Tactic:
h'

Goal state after:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ f (c i) ≤ f (ωSup₀ c)

Tactic:
h'

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ f (c i) ≤ ωSup (c.map f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), c i ≤ x
⊢ f (ωSup₀ c) ≤ f x

Tactic:
h'

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), c i ≤ x
⊢ ωSup (c.map f) ≤ f x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
· right; exact le_trans hyz (le_map z)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
⊢ y < x → f y ≤ x

Tactic:
hyx

Goal state after:
case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
hyx : y < x
⊢ f y ≤ x
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a \ b).get hab = a.get ⋯ \ b.get ⋯

Tactic:
by
  simp [sdiff_def]; aesop

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
⊢ f y ≤ cSup c

Tactic:
have hc' := (bot_isAdmissible le_map).cSup_mem _ (subset_trans hc fun _ h ↦ h.mem_bot)
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hc'
      apply hc'.2.resolve_left
      intro hc'
      exact lt_irrefl y (lt_of_lt_of_le hy' hc')

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
⊢ ∀ (a b c : Cardinal.{u}), a ≤ b → b ≤ c → a ≤ c

Tactic:
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨e₁⟩ ⟨e₂⟩
    exact ⟨e₁.trans e₂⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
⊢ #(Set α) = 2 ^ #α

Tactic:
by
  simp [← mk_congr (Equiv.ofBijective _ Set.ofPred_bijective), ← one_add_one_eq_two]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a✝ : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
h_a : f a ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
exact ωSup_iterate_le_prefixedPoint f x h h_a h_x_le_a

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ 0 • x = 0

Tactic:
rw [← f.map_zero, hsmul, zero_smul]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M (a * b)

Tactic:
rw [h]; exact one M

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝³ : AddZeroClass A
inst✝² : AddZeroClass B
inst✝¹ : AddZeroClass C
inst✝ : DistribSMul M B
r : M
f : A →+ B
x✝¹ x✝ : A
⊢ r • f (x✝¹ + x✝) = r • f x✝¹ + r • f x✝

Tactic:
by simp only [map_add, smul_add]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hr : r ≠ 0
hm : m ≠ 0
⊢ r • m ≠ 0

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m = 0 ↔ r = 0

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m ≠ 0 ↔ r ≠ 0

Tactic:
by simp [*]

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

Goal state before:
pp: case mem
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ ↑⟨p.toAddSubmonoid, ⋯⟩
⊢ t • x ∈ ⨆ a, ↑a

Tactic:
suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)

Goal state after:
case mem
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ ↑⟨p.toAddSubmonoid, ⋯⟩
⊢ p.toAddSubmonoid ≤ ⨆ q, ↑q
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ f (a ⊔ b) = f a ⊔ f b

Tactic:
rw [← sSup_pair, map_sSup]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ sSup (⇑f '' {a, b}) = f a ⊔ f b
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
⊢ f ⊥ = ⊥

Tactic:
rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty]

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ sSup ((fun x ↦ f (g x)) '' s) = sSup (⇑f ∘ ⇑g '' s)

Tactic:
simp only [Function.comp]

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : FunLike F α β
f : α → β
s : Set (Set β)
⊢ ⋃ t ∈ s, f ⁻¹' t = sSup (preimage f '' s)

Tactic:
simp only [Set.sSup_eq_sUnion, Set.sUnion_image]

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun x ↦ x.1 ⊓ x.2) '' s)

Tactic:
Prod.fst_sInf,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ sInf (Prod.fst '' s) ⊓ (sInf s).2 = sInf ((fun x ↦ x.1 ⊓ x.2) '' s)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ sInf (Prod.fst '' s) ⊓ sInf (Prod.snd '' s) = sInf ((fun x ↦ x.1 ⊓ x.2) '' s)

Tactic:
sInf_image,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (⨅ a ∈ s, a.1) ⊓ ⨅ a ∈ s, a.2 = ⨅ a ∈ s, a.1 ⊓ a.2
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x y : M
⊢ x - y ∈ f.ker ↔ f x = f y

Tactic:
rw [mem_ker, map_sub, sub_eq_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
val✝ : M
h₁ : val✝ ∈ p
h₂ : ⟨val✝, h₁⟩ ∈ ↑(comap p.subtype p')
⊢ p.subtype ⟨val✝, h₁⟩ ∈ p ⊓ p'

Tactic:
exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.Algebra.Ring.ULift

Goal state before:
pp: R : Type u
inst✝ : Distrib R
x✝² x✝¹ x✝ : ULift R
⊢ Equiv.ulift ((x✝² + x✝¹) * x✝) = Equiv.ulift (x✝² * x✝ + x✝¹ * x✝)

Tactic:
simp [right_distrib]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : f₁ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
h₂ : f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ

Tactic:
exact ⟨h₁, h₂⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
apply FaithfulSMul.algebraMap_injective R A
    rw [algebraMap.smul', map_add, smul_add, ← algebraMap.smul', ← algebraMap.smul', ← map_add]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
φ : A →ₐ[R] B
⊢ φ.comp (ofId R A) = ofId R B

Tactic:
by ext

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

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M →ₗ[R] N
r : S
x : M
⊢ f.toFun (r • x) = (RingHom.id S) r • f.toFun x

Tactic:
obtain ⟨r, rfl⟩ := h r; simp

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

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M ≃ₗ[R] N
r : S
x : M
⊢ (↑f).toFun (r • x) = (RingHom.id S) r • (↑f).toFun x

Tactic:
obtain ⟨r, rfl⟩ := h r; simp

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

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
⊢ x * a = 0 → x = 0

Tactic:
h'

Goal state after:
case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
⊢ x * b = 0 → x = 0

Tactic:
h'

Goal state after:
case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Associates M
⊢ Associates.mk (Quot.out a) = a

Tactic:
rw [← quot_mk_eq_mk, Quot.out_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Quot.out (Associates.mk a) ~ᵤ a

Tactic:
by
  rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]

Goal state after: