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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
⊢ _root_.commutator G ≤ N

pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'

Tactic:
· rw [commutator_eq_normalClosure, ← Subgroup.normalClosure_subset_iff]
    rintro x ⟨p, q, rfl⟩
    rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]
    simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]
    rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
⊢ ↑u * ↑s₂ ∈ S

Tactic:
← S.coe_mul

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
⊢ ↑(u * s₂) ∈ S
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ (f.lift hg) x✝ = j x✝

Tactic:
rw [lift_spec, ← hj, ← hj, ← j.map_mul]

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ j (f (f.sec x✝).1) = j (f ↑(f.sec x✝).2 * x✝)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S) x y ↔ (OreLocalization.oreEqv S M) x y

Tactic:
simp +instances only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv,
    smul_eq_mul, Submonoid.mk_smul]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) ↔ ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ Surjective ⇑(f.lift hg) → ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1

Tactic:
intro H v

Goal state after:
case mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : Surjective ⇑(f.lift hg)
v : P
⊢ ∃ x, v * g ↑x.2 = g x.1
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ (∀ (v : P), ∃ x, v * g ↑x.2 = g x.1) → Surjective ⇑(f.lift hg)

Tactic:
intro H v

Goal state after:
case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
⊢ ∃ a, (f.lift hg) a = v
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
⊢ ↑s₄' * (r₃' * ↑s₁') * ↑s ∈ S

Tactic:
← h₃,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
⊢ ↑s₄' * (↑s₃' * (↑s₂' * r₂)) * ↑s ∈ S
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑s₄' * (r₃' * ↑s₁') * ↑s = ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s

Tactic:
← h₃,

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑s₄' * (↑s₃' * (↑s₂' * r₂)) * ↑s = ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccPrelimit a ↔ a ∈ range succ

Tactic:
simp_rw [isSuccPrelimit_iff_succ_ne, not_forall, not_ne_iff, mem_range]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) = ⨅ x, ↑x

Tactic:
iInf,

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) = sInf (range fun x ↦ ↑x)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ ¬IsMax (succ^[n - 1] i)

Tactic:
rcases n with - | n

Goal state after:
case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
hn : ¬IsMax (succ^[0 - 1] i) → pred^[0] (succ^[0] i) = i
hin : ¬IsMax (succ^[0] i)
⊢ ¬IsMax (succ^[0 - 1] i)

case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n + 1 - 1] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ ¬IsMax (succ^[n + 1 - 1] i)
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type v
inst✝ : Subsingleton α
⊢ Small.{w, v} α

Tactic:
rcases isEmpty_or_nonempty α with ⟨⟩

Goal state after:
case inl
α : Type v
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ Small.{w, v} α

case inr
α : Type v
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ Small.{w, v} α
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : ⟨b, hb⟩ < ⟨c, hc⟩
⊢ ⟨b, hb⟩ ≤ if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩

Tactic:
Subtype.mk_lt_mk

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
⊢ ⟨b, hb⟩ ≤ if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
i : Fin n
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
rcases n with - | n

Goal state after:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
i : Fin 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ {x ∈ T | x.length = s} ⊆ image List.ofFn univ

Tactic:
intro a ha

Goal state after:
α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
⊢ a ∈ image List.ofFn univ
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C u v w

Tactic:
induction n with
  | zero =>
    rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
    cases u_property
    rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
    cases w_property
    apply
      @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
        ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Tactic:
exact fun a ha ha' => h <| ha'.symm ▸ ha

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

Goal state before:
pp: a : Cardinal.{u}
⊢ Nonempty (Quotient.out (lift.{v, u} a) ≃ Quotient.out a)

Tactic:
rw [← mk_out a, ← mk_uLift, mk_out]

Goal state after:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift (Quotient.out a)) ≃ Quotient.out a)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : IsLUB d (p₁, p₂)
⊢ IsLUB ((fun b ↦ b.1 ⊔ b.2) '' d) ((fun b ↦ b.1 ⊔ b.2) (p₁, p₂))

Tactic:
simp only [IsLUB, IsLeast, upperBounds, Prod.forall, mem_ofPred_eq, Prod.mk_le_mk] at hdp
  simp only [IsLUB, IsLeast, upperBounds, mem_image, Prod.exists, forall_exists_index, and_imp]
  have e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2
  simp only [lowerBounds, mem_ofPred_eq, Prod.forall, Prod.mk_le_mk] at e1
  refine ⟨fun a b₁ b₂ hbd hba => ?_,fun b hb => ?_⟩
  · rw [← hba]
    exact sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2
  · rw [sup_le_iff]
    exact e1 _ _ fun b₁ b₂ hb' => sup_le_iff.mp (hb b₁ b₂ hb' rfl)

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)
  · rw [h]
    left
    apply OrderBot.bot_le _
  right; intro b' h₁
  rw [Part.eq_some_iff] at h₀
  have hx := hx _ h₀; have hy := hy _ h₁
  have hx := Part.mem_unique hx hy; subst hx
  exact h₀

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯

Tactic:
ext n : 2; cases n <;> rfl

Goal state after:
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) ≤ ωSup (c.map f)

Tactic:
apply le_ωSup (c.map f)

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

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

Tactic:
rintro ⟨α⟩

Goal state after:
case mk
α✝ β : Type u
a✝ : Cardinal.{u}
α : Type u
⊢ Quot.mk (⇑isEquivalent) α ≤ Quot.mk (⇑isEquivalent) α
Module: Mathlib.SetTheory.Cardinal.Order

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

Tactic:
rintro ⟨α⟩

Goal state after:
case mk
α✝ β : Type u
a✝ : Cardinal.{u}
α : Type u
⊢ 0 ≤ Quot.mk (⇑isEquivalent) α
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
⊢ toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀

Tactic:
by simp [not_or]

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

Goal state before:
pp: case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ (sum fun x ↦ ↑(e.symm x)) ∈ upperBounds s

Tactic:
intro a ha

Goal state after:
case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
a : Cardinal.{u}
ha : a ∈ s
⊢ a ≤ sum fun x ↦ ↑(e.symm x)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inl
α : Type u_1
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
t : Finset α
h : ↑t.card ≤ #α
⊢ ∃ s, t.card = s.card

Tactic:
exact ⟨t, rfl⟩

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

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
⊢ #↑(T \ S) ≠ 0

Tactic:
intro h'

Goal state after:
α : Type u
S T : Set α
h : #↑S < #↑T
h' : #↑(T \ S) = 0
⊢ False
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : (fun x ↦ s • x) x = (fun x ↦ s • x) y
⊢ x = y

Tactic:
refine (?_ : IsRegular (s • 1 : R)).isSMulRegular (by simpa using hxy)

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : (fun x ↦ s • x) x = (fun x ↦ s • x) y
⊢ IsRegular (s • 1)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' ^ n)
⊢ Surjective ⇑f'

Tactic:
← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn),

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' ^ n.pred.succ)
⊢ Surjective ⇑f'
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(⨅ i, p i) = ⋂ i, ↑(p i)

Tactic:
iInf,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(sInf (Set.range fun i ↦ p i)) = ⋂ i, ↑(p i)
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
⊢ sSup (⇑f '' ∅) = ⊥

Tactic:
Set.image_empty,

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
⊢ sSup ∅ = ⊥
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: case inl
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 α
x✝ : CompleteLattice β
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' ∅)

Tactic:
Set.image_empty,

Goal state after:
case inl
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 α
x✝ : CompleteLattice β
⊢ ⊥ = sSup ∅
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
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy : y' ∈ Submodule.map (↑e) p
⊢ ↑e.symm ↑⟨y', hy⟩ ∈ p

Tactic:
rw [Submodule.mem_map] at hy

Goal state after:
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
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy✝ : y' ∈ Submodule.map (↑e) p
hy : ∃ y ∈ p, ↑e y = y'
⊢ ↑e.symm ↑⟨y', hy✝⟩ ∈ p
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case neg
M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

Tactic:
· simpa [h] using! id

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

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ (a + b) * (x✝¹ * x✝) = (a + b) * x✝¹ * x✝

Tactic:
by rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ s
⊢ x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)

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

Goal state before:
pp: case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a ~ᵤ a * c

Tactic:
have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]

Goal state after:
case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
⊢ a ~ᵤ a * c
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case inr
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Nontrivial M₀
⊢ Submonoid.map f S ≤ M₀'⁰

Tactic:
· refine le_nonZeroDivisors_of_noZeroDivisors ?_
    rintro ⟨x, hx, hx0⟩
    exact zero_notMem_nonZeroDivisors <| hS <| map_eq_zero_iff f hf |>.mp hx0 ▸ hx

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
H : ¬s = 0 ∧ t ≠ 0
hst : (s * t).Nonempty
⊢ False

Tactic:
← hst.of_smul_left.subset_zero_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : ¬s ⊆ 0 ∧ t ≠ 0
hst : (s * t).Nonempty
⊢ False
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
⊢ z ∈ p

Tactic:
rw [← SetLike.mem_coe, coe_range, Set.mem_range] at h₁

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : ∃ y_1, f y_1 = y
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
⊢ z ∈ p
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint c (b ⊔ a)

Tactic:
apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm

Goal state after:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : AddSubmonoid M
⊢ (span ℕ ↑s).toAddSubmonoid = s

Tactic:
span_nat_eq_addSubmonoidClosure,

Goal state after:
M : Type u_4
inst✝ : AddCommMonoid M
s : AddSubmonoid M
⊢ AddSubmonoid.closure ↑s = s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ↑{x} ⊆ S

Tactic:
rwa [Finset.coe_singleton, Set.singleton_subset_iff]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∃ s_1, IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a

Tactic:
by
    classical
    refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
    rw [isLUB_pi]
    intro i
    simp_rw [isAtom_iff_eq_single]
    refine ⟨?_, ?_⟩
    · rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
      exact hs i
    · refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
      exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)

Tactic:
rw [insert_sdiff_of_mem _ (mem_singleton _), sdiff_singleton_eq_self hxy] at this

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup y)
⊢ Disjoint x (sSup y)