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

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * ↑s ∈ S
⊢ oreNum (c • 1) s • r /ₒ (oreDenom (c • 1) s * 1) =
    oreNum (c • 1) ⟨t * ↑s, ht⟩ • t • r /ₒ oreDenom (c • 1) ⟨t * ↑s, ht⟩

Tactic:
← oreDiv_smul_oreDiv,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * ↑s ∈ S
⊢ (c • 1 /ₒ 1) • (r /ₒ s) = oreNum (c • 1) ⟨t * ↑s, ht⟩ • t • r /ₒ oreDenom (c • 1) ⟨t * ↑s, ht⟩
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * ↑s ∈ S
⊢ (c • 1 /ₒ 1) • (r /ₒ s) = oreNum (c • 1) ⟨t * ↑s, ht⟩ • t • r /ₒ (oreDenom (c • 1) ⟨t * ↑s, ht⟩ * 1)

Tactic:
← oreDiv_smul_oreDiv,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * ↑s ∈ S
⊢ (c • 1 /ₒ 1) • (r /ₒ s) = (c • 1 /ₒ 1) • (t • r /ₒ ⟨t * ↑s, ht⟩)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0

Tactic:
simp [pow_eq_top_iff, or_iff_not_imp_left]

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

Goal state before:
pp: case inr.inl
α : 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₁ * ↑b₁ < a₂ * ⊤

Tactic:
rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]
    exact coe_lt_top _

Goal state after:
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 α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x✝ : 1 ≠ 0
⊢ StrictMono fun a ↦ a ^ 1

Tactic:
by simpa only [pow_one] using! strictMono_id

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
⊢ IsSuccPrelimit a

Tactic:
by
  intro b hb
  obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
  obtain rfl := (hb.ge_of_gt hbc).antisymm hca
  contradiction

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ Order.pred^[b - a] b = a

Tactic:
pred_eq_pred,

Goal state after:
m n a b : ℕ
h : a ≤ b
⊢ pred^[b - a] b = a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : LinearOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x + 1 = y + 1 ↔ x = y

Tactic:
simp [← succ_eq_add_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
⊢ a ≤
    match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)

Tactic:
obtain - | a := a
    · exact le_top
    change _ ≤ ite _ _ _
    split_ifs
    · exact le_top
    · exact coe_le_coe.2 (le_succ a)

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

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b

pp: case neg
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : ¬IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b

Tactic:
· rw [pred_eq_iff_isMin.2 ha']
      exact hn this

Goal state after:
case neg
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : ¬IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
⊢ MonotoneOn f s

Tactic:
rintro a ha b hb hab
  obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab
  clear hab
  induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)

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

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
x : ℕ
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa [hf.eq_iff' (map_zero f)] using hx

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

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

pp: case neg
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : ¬IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
· rw [pred_eq_iff_isMin.2 ha']
      exact hn this

Goal state after:
case neg
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : ¬IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : ¬IsMin b
⊢ f (pred^[n + 1] b) < f b

Tactic:
induction n with
  | zero => simpa using hf _ hab hb ha
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n + 1] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)

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

Goal state before:
pp: case inr.inr.coe
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
x : ℕ
hx : ↑x ≠ 0
⊢ map (⇑f) (↑x * y) = map ⇑f ↑x * map (⇑f) y

Tactic:
induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -natCast_mul]

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

Goal state before:
pp: case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m

Tactic:
WithBot.coe_lt_coe,

Goal state after:
case coe
m : ℕ
a✝ : ℕ∞
⊢ a✝ < ↑(m + 1) ↔ ↑a✝ ≤ ↑m
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
⊢ ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

Tactic:
prod_eq_mul_prod_sdiff_singleton_of_mem h,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
⊢ f i * ∏ x ∈ s \ {i}, f x = (∏ x ∈ s \ {i}, f x) * f i
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i

Tactic:
obtain ⟨g', hg'⟩ := H hfst' hfs'

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u_1 → Type u_2
AF : Applicative F
inst✝ : LawfulApplicative F
α✝ β✝ : Type u_1
f : F (α✝ → β✝)
x : F α✝
⊢ id <$> f <*> x = f <*> x

Tactic:
rw [id_map]

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : ℕ
hi : i < n
⊢ (map f v)[i] = f v[i]

Tactic:
by
  simp only [getElem_def, toList_map, List.getElem_map]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
⊢ ↑(replicate n a) = Multiset.replicate n a

Tactic:
rw [val_eq_coe, coe_replicate]

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨i + 1, ⋯⟩

Tactic:
rcases x with ⟨_ | _, h⟩ <;> try rfl

Goal state after:
case nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h : [].length = n
⊢ (tail ⟨[], h⟩).get ⟨i, ih⟩ = get ⟨[], h⟩ ⟨i + 1, ⋯⟩
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (n✝ + 1)
⊢ s = s'

Tactic:
obtain ⟨b, -⟩ := exists_mem s

Goal state after:
case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b✝ : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (n✝ + 1)
b : α
⊢ s = s'
Module: Mathlib.Data.Vector.Basic

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

Tactic:
simp [scanl_singleton, i0, get_zero]

Goal state after:
case succ.zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (0 + 1)
i : Fin (0 + 1)
i0 : i = 0
⊢ (b ::ᵥ f b v.head ::ᵥ nil).get 1 = f b v.head
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 ≤ (↑⟨l, hl⟩).length

Tactic:
· rw [hl]
      exact Nat.le_of_succ_le_succ j.2

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

Goal state before:
pp: case mk.mk.mk.h
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ val✝¹ ≠ val✝

Tactic:
· simpa using h

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

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
⊢ Nonempty (Quotient.out x)

Tactic:
by
  rwa [← mk_ne_zero_iff, mk_out]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
a b : (α ⊕ β) ⊕ γ
⊢ (Equiv.sumAssoc α β γ) a ≤ (Equiv.sumAssoc α β γ) b ↔ a ≤ b

Tactic:
by
      rcases a with ((_ | _) | _) <;> rcases b with ((_ | _) | _) <;>
      simp [Equiv.sumAssoc]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b ↑(collapseF f a)

Tactic:
by
  rw [collapseF, IsWellFounded.fix_eq]
  dsimp only
  exact WellFounded.not_lt_min _ {b | ∀ a', r a' a → s (collapseF f a') b} h

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast (bot x f) x

Tactic:
by
    constructor
    · exact fun _ h ↦ h.base_isLeast.1
    · intro y hy
      exact hy (Ici x) (ici_isAdmissible le_map)

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {α β : Type u_4}, Functor.mapConst = Functor.map ∘ const β

Tactic:
by simp [Functor.mapConst, Functor.map]

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

Goal state before:
pp: case succ
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
⊢ SuccChain r s✝ = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
| succ _ ih =>

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ ωScottContinuous f ↔ ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

Tactic:
refine ⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })) → ωScottContinuous f
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
← hc

Goal state after:
case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB ((fun c ↦ Set.range ⇑c) c) a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (∀ (x x_1 : ℕ), f (c x_1) ≤ a ∨ g (c x) ≤ a) ↔ ∀ (i : ℕ), f (c i) ≤ a ∨ g (c i) ≤ a

Tactic:
exact ⟨fun h _ ↦ h _ _, fun h i j ↦
    (h (max j i)).imp (le_trans <| hf.monotone <| c.mono <| le_max_left _ _)
      (le_trans <| hg.monotone <| c.mono <| le_max_right _ _)⟩

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
⊢ False

Tactic:
by
    have : Inhabited (∀ i : ι, (g i).out) := by
      refine ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 ?_⟩
      rw [mk_out]
      exact (H i).ne_bot
    let G := invFun F
    have sG : Surjective G := invFun_surjective F.2
    choose C hc using
      show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b by
        intro i
        simp only [not_exists.symm, not_forall.symm]
        refine fun h => (H i).not_ge ?_
        rw [← mk_out (f i), ← mk_out (g i)]
        exact ⟨Embedding.ofSurjective _ h⟩
    let ⟨⟨i, a⟩, h⟩ := sG C
    exact hc i a (congr_fun h _)

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

Goal state before:
pp: α : Type (max u v)
inst✝ : Small.{v, max u v} α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α

Tactic:
rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
rintro ⟨ha, hb⟩
    exact ⟨ha.mul hb, hb.mul ha⟩

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * (y * (algebraMap R A) r) = x * y * (algebraMap R A) r

Tactic:
← mul_assoc

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * y * (algebraMap R A) r = x * y * (algebraMap R A) r
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ (g ∘ₛₗ 0) c = 0 c

Tactic:
rw [comp_apply, zero_apply, zero_apply, g.map_zero]

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
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ n • a

Tactic:
by
    simp_rw [← Nat.cast_smul_eq_nsmul R]; apply smul_right_injective; simpa

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
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
x : M
hx : x ∈ p
hxy : ↑e x = y'
⊢ ↑e.symm ↑⟨y', hy⟩ ∈ p

Tactic:
subst hxy

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
x : M
hx : x ∈ p
hy : ↑e x ∈ Submodule.map (↑e) p
⊢ ↑e.symm ↑⟨↑e x, hy⟩ ∈ p
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
hb : b ∈ closure ↑S
⊢ a * b ∈ closure ↑S

Tactic:
by
  induction hb using closure_induction with
  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
  | zero => simp only [mul_zero, zero_mem _]
  | add r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ⇑f
x : ↥f.srange
x' : M
hx' : f x' = ↑x
⊢ f (g ↑x) = ↑x

Tactic:
← hx',

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ⇑f
x : ↥f.srange
x' : M
hx' : f x' = ↑x
⊢ f (g (f x')) = f x'