mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ BddAbove (g '' f '' s)

Tactic:
simpa [bddAbove_def] using hf

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b

Tactic:
by
  rcases h2.eq_or_lt with (h2 | h2); · exact Or.inl h2.symm
  rcases h3.eq_or_lt with (h3 | h3); · exact Or.inr h3
  exact (h.2 h2 h3).elim

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : ∀ (x : α), a ≤ x ∧ x < b ↔ x = c
⊢ a = c ∧ a ⋖ b

Tactic:
have ⟨hac, hcb⟩ := (h c).mpr rfl

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : ∀ (x : α), a ≤ x ∧ x < b ↔ x = c
hac : a ≤ c
hcb : c < b
⊢ a = c ∧ a ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), a < x ∧ x < b ↔ x = c
⊢ a ⋖ c ∧ c ⋖ b

Tactic:
have ⟨hac, hcb⟩ := (h c).mpr rfl

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), a < x ∧ x < b ↔ x = c
hac : a < c
hcb : c < b
⊢ a ⋖ c ∧ c ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂

Tactic:
refine ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩
  have : c.2 = b := h₂.le.2.antisymm h₁.le.2
  rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂
  exact h h₁ h₂

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ s.preimage f hf ⊆ t

Tactic:
rw [← coe_subset, coe_preimage]

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ f ⁻¹' ↑s ⊆ ↑t
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico c b = Ico a (min b c)

Tactic:
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_sdiff_Ico_right]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ #(Iio b) = b

Tactic:
Iio_eq_Ico,

Goal state after:
b : ℕ
⊢ #(Ico ⊥ b) = b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
simp only [sSup,
        mem_empty_iff_false, IsEmpty.forall_iff, forall_const, exists_const, dite_true]

Goal state after:
s : Set ℕ
hs : ¬BddAbove s
⊢ (if h : ∃ n, ∀ a ∈ s, a ≤ n then Nat.find h else 0) = Nat.find ⋯
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
classical
    have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
      simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
    cases this
    exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
      ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨g, gmon⟩ := h f
    exact ⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_1
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ ∅, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)

pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ i ∈ Finset.cons a s h, r i ((f ∘ ⇑g) a_2 i) ((f ∘ ⇑g) b i)

Tactic:
· intro f
    exists RelEmbedding.refl (· ≤ ·)
    simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]

Goal state after:
case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ i ∈ Finset.cons a s h, r i ((f ∘ ⇑g) a_2 i) ((f ∘ ⇑g) b i)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.WellFoundedOn r ↔ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
have f : RelEmbedding (Subrel r (· ∈ s)) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
    ⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩
  refine ⟨fun h => ?_, f.wellFounded⟩
  rw [WellFounded.wellFounded_iff_has_min]
  intro t ht
  by_cases hst : (s ∩ t).Nonempty
  · rw [← Subtype.preimage_coe_nonempty] at hst
    rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩
    exact ⟨m, mt, fun x xt ⟨xm, xs, _⟩ => hm ⟨x, xs⟩ xt xm⟩
  · rcases ht with ⟨m, mt⟩
    exact ⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b

Tactic:
by
  rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (↑(Submonoid.closure s)).IsPWO

Tactic:
Submonoid.closure_eq_image_prod

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (List.prod '' {l | ∀ x ∈ l, x ∈ s}).IsPWO
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → s.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
rw [wellFoundedOn_iff_no_descending_seq]

Goal state after:
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2), ¬∀ (n : ℕ), f n ∈ s
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c

Tactic:
exact Set.eq_of_mem_uIcc_of_mem_uIcc'

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : n < g 0
⊢ List.SublistForall₂ r (f m) (f n)

Tactic:
if_pos hn,

Goal state after:
case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn : List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail) (f n)
hn : n < g 0
⊢ List.SublistForall₂ r (f m) (f n)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ n * (s * ↑(closure s)) = ↑(closure s)

Tactic:
mul_subgroupClosure hs,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ n * ↑(closure s) = ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid

Tactic:
· simp only [true_and, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) → x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝

Tactic:
rintro ⟨y, ⟨hyA, hyB⟩, z, hz, rfl⟩
    refine ⟨A.mul_mem hyA (h hz), ?_⟩
    exact ⟨y, hyB, z, hz, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ r x y

Tactic:
rw [← hr]

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ c.toSetoid x y
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = tl2.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
L₅ : List (α × Bool)
H3 : Step (tl ++ x✝⁵) L₅
H4 : Step (tl2 ++ x✝⁴) L₅
⊢ Step ((x4, b4) :: tl2 ++ x✝⁴) ((x3, b3) :: L₅)

Tactic:
simpa [H1] using Step.cons H4

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) = (a * c)⁻¹ * (b * d)

Tactic:
by
        simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s t : Finset M
⊢ closure ↑(s ∪ t) = closure ↑s ⊔ closure ↑t

Tactic:
simp [closure_union]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ ↑x = 1 ↔ x ∈ N

Tactic:
refine QuotientGroup.eq.trans ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
s t : Finset G
⊢ closure ↑(s ∪ t) = closure ↑s ⊔ closure ↑t

Tactic:
simp [closure_union]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
G : Type u_3
H : Type u_4
inst✝⁵ : Group G
inst✝⁴ : AddGroup H
inst✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG M
inst✝ : FG N
⊢ ⊤.FG

Tactic:
← Submonoid.top_prod_top

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
G : Type u_3
H : Type u_4
inst✝⁵ : Group G
inst✝⁴ : AddGroup H
inst✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG M
inst✝ : FG N
⊢ (⊤.prod ⊤).FG
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ Prod.mk <$> 0 <*> y = (fun b a ↦ (a, b)) <$> y <*> 0

Tactic:
rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of s * of t = of t * of s

Tactic:
| of t =>

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk m₁ s₁ / mk m₂ s₂ = mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩

Tactic:
simp [div_eq_mul_inv, mk_mul]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk (m₁ * ↑s₂) (s₁ * ⟨m₂, ⋯⟩) = mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩
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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
⊢ r₁' • r₁ /ₒ (s₁' * s) = r₂' • r₂ • r₁ /ₒ (s₂' * s)

Tactic:
rcases oreCondition (s₁' : R) (s₂') with ⟨r₃', s₃', 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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
⊢ r₁' • r₁ /ₒ (s₁' * s) = r₂' • r₂ • r₁ /ₒ (s₂' * 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
P : Type u_3
inst✝² : CommMonoid P
f : M → N
hf : S.IsLocalizationMap f
E : Type u_4
inst✝¹ : EquivLike E N P
inst✝ : MulEquivClass E N P
e✝ : E
y : P
e : N ≃* P := ↑e✝
x : M × ↥S
eq : e.symm y * f ↑x.2 = f x.1
⊢ e.symm (y * (⇑e✝ ∘ f) ↑x.2) = e.symm ((⇑e✝ ∘ f) x.1)

Tactic:
simpa [e]

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

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = a✝¹ * untopD 0 ↑a✝

Tactic:
untopD_coe

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = a✝¹ * a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ a₂ ≠ 0

Tactic:
by simpa [bot_eq_zero] using ha.bot_lt.ne'

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

Goal state before:
pp: case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 ⊥ = unbotD 0 ⊥ * unbotD 0 b

Tactic:
unbotD_bot,

Goal state after:
case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ 0 = 0 * unbotD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ unbotD 0 ⊥ = unbotD 0 ↑a✝ * unbotD 0 ⊥

Tactic:
unbotD_bot,

Goal state after:
case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ 0 = unbotD 0 ↑a✝ * 0
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b

Tactic:
· rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]
    apply lt_succ_of_le_of_not_isMax h hb

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : ¬IsMax x
⊢ x + 1 ≤ y ↔ x < y

Tactic:
rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]

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

Goal state before:
pp: n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + 1 ↔ n ≤ ↑m

Tactic:
by
  rw [← WithBot.coe_one, ← ENat.natCast_one, WithBot.coe_natCast, ← Nat.cast_add,
    ← WithBot.coe_natCast]
  cases n
  · simp only [bot_le, WithBot.bot_lt_coe]
  · rw [WithBot.coe_lt_coe, Nat.cast_add, natCast_one, ENat.lt_add_one_iff (natCast_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
b : M
⊢ ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x

Tactic:
by
  rw [update_eq_piecewise, prod_piecewise]
  simp [h]

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

Goal state before:
pp: case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ n

Tactic:
exact Nat.le_of_succ_le_succ j.2

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (map₂ f (a✝ ::ᵥ x✝) (b✝ ::ᵥ y✝)).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Tactic:
rw [map₂_cons]
    cases i using Fin.cases
    · simp only [get_zero, head_cons]
    · simp only [get_cons_succ, ih]

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ↑n = toENat c ↔ ↑n = c

Tactic:
simp [eq_comm (a := Nat.cast _)]

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_1}
⊢ c < ↑n + 1 ↔ c ≤ ↑n

Tactic:
← Order.lt_succ_iff,

Goal state after:
n : ℕ
c : Cardinal.{u_1}
⊢ c < ↑n + 1 ↔ c < succ ↑n
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✝³ : Zero A
inst✝² : Zero B
inst✝¹ : Zero C
inst✝ : SMulZeroClass M B
r : M
f : ZeroHom A B
⊢ r • f 0 = 0

Tactic:
by simp only [map_zero, smul_zero]

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
⊢ r • f 0 = 0

Tactic:
by simp only [map_zero, smul_zero]

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

Goal state before:
pp: S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid V
inst✝¹³ : Module R V
inst✝¹² : Module S V
inst✝¹¹ : AddCommMonoid W
inst✝¹⁰ : Module R W
inst✝⁹ : Module S W
inst✝⁸ : AddCommMonoid G
inst✝⁷ : Module R G
inst✝⁶ : Module S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
x✝ : G
⊢ ((α • e) ≪≫ₗ f) x✝ = (α • e ≪≫ₗ f) x✝

Tactic:
simp [LinearMapClass.map_smul_of_tower f]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ ((fun m ↦ { toFun := fun x ↦ m * x, map_smul' := ⋯ }) ((fun f ↦ f 1) f)) m = f m

Tactic:
change MulOpposite.op m • f 1 = _

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ MulOpposite.op m • f 1 = f m
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
⊢ 0 ∈ C

Tactic:
obtain ⟨x, hx⟩ := nonempty
    simpa [zero_smul, add_zero] using linearComb x hx x hx 0 0

Goal state after:
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
⊢ ⊥.toAddSubmonoid = ⊤.toAddSubmonoid ↔ ⊥ = ⊤

Tactic:
bot_toAddSubmonoid,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥ = ⊤.toAddSubmonoid ↔ ⊥ = ⊤
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ⊔ g.ker ≤ (f ∘ₗ g).ker

Tactic:
refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ≤ (f ∘ₗ g).ker
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
⊢ (funLeft R M ⇑e ∘ₗ funLeft R M ⇑e.symm) x i = LinearMap.id x i

Tactic:
id_apply,

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
⊢ (funLeft R M ⇑e ∘ₗ funLeft R M ⇑e.symm) x i = x i
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
⊢ (funLeft R M ⇑e.symm ∘ₗ funLeft R M ⇑e) x i = LinearMap.id x i

Tactic:
id_apply,

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
⊢ (funLeft R M ⇑e.symm ∘ₗ funLeft R M ⇑e) x i = x i
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
by simpa only [← hm] using! sm.mul_mem

Goal state after: