mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case mk.mk
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
val✝¹ : Multiset α
sl : List α
hsl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) sl)
val✝ : Multiset α
tl : List α
htl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) tl)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl }
    { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }
comm :
  (↑({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl })).Pairwise
    (Commute on f)
⊢ ({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }).noncommProd
      f comm =
    { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl }.noncommProd f ⋯ *
      { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }.noncommProd f ⋯

Tactic:
simp only [← Finset.disjoint_val, Multiset.quot_mk_to_coe'] at h

Goal state after:
case mk.mk
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
val✝¹ : Multiset α
sl : List α
hsl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) sl)
val✝ : Multiset α
tl : List α
htl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) tl)
comm :
  (↑({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl })).Pairwise
    (Commute on f)
h : Disjoint ↑sl ↑tl
⊢ ({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }).noncommProd
      f comm =
    { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl }.noncommProd f ⋯ *
      { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }.noncommProd f ⋯
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : { d // c ≤ d }
⊢ c ≤ ↑d

Tactic:
exact d.2

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
c : Con G
x✝ : G
h : x✝ ∈ {x | c x 1}
⊢ x✝⁻¹ ∈ {x | c x 1}

Tactic:
by simpa using c.inv h

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

Goal state before:
pp: case e'_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
s : Multiset M
⊢ s = Multiset.map id s

Tactic:
rw [Multiset.map_id]

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
ι : Type u_5
inst✝² : Finite ι
G : ι → Type u_6
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), Group.FG (G i)
⊢ ⊤.FG

Tactic:
rw [← Subgroup.pi_top Set.univ]

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
ι : Type u_5
inst✝² : Finite ι
G : ι → Type u_6
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), Group.FG (G i)
⊢ (Subgroup.pi Set.univ fun i ↦ ⊤).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
f : κ → M
g : ι → κ
⊢ ∏ a ∈ s, f (g a) = ∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b})

Tactic:
by
  simp_rw [← prod_const, prod_fiberwise_of_maps_to' fun _ ↦ mem_image_of_mem _]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₂ ↦ of (1 * x₂)) (of L) = of L
⊢ (lift fun x₂ ↦ of (1 * x₂)) (-of L) = -of L

Tactic:
| neg L ih =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₁ ↦ of (x₁ * 1)) (of L) = of L
⊢ (lift fun x₁ ↦ of (x₁ * 1)) (-of L) = -of L

Tactic:
| neg L ih =>

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

Goal state before:
pp: case h
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ↑h * g * (↑h)⁻¹ * g⁻¹ = g

Tactic:
hg

Goal state after:
case h
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case h₁
G : Type u_1
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G

pp: case h₂
G : Type u_1
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)

Tactic:
· rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
    exact ⟨g₁, g₂, rfl⟩

Goal state after:
case h₂
G : Type u_1
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)
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
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : ↑c * x = ↑c * y
⊢ f x = f y

Tactic:
replace h := congr_arg f h
    rw [map_mul, map_mul] at h
    exact (f.map_units c).mul_right_inj.mp h

Goal state after:
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
x : M
y : ↥S
⊢ f ↑y * f.mk' x y = f x

Tactic:
rw [mul_comm, mk'_spec]

Goal state after:
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : k (d * x) = k d * k y
hd : k d = ↑c
⊢ ↑⟨d, ⋯⟩ * x = ↑⟨d, ⋯⟩ * y

Tactic:
← map_mul k

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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : k (d * x) = k (d * y)
hd : k d = ↑c
⊢ ↑⟨d, ⋯⟩ * x = ↑⟨d, ⋯⟩ * y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.coe
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
x : R
hx : ↑x ≠ 0
⊢ map (⇑f) (↑x * y) = map ⇑f ↑x * map (⇑f) y

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

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 α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
by
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
  lift a₁ to α using ha.lt_top.ne
  lift b₁ to α using hb.lt_top.ne
  obtain rfl | ha₂ := eq_or_ne a₂ ⊤
  · rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]
    exact coe_lt_top _
  obtain rfl | hb₂ := eq_or_ne b₂ ⊤
  · rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]
    exact coe_lt_top _
  lift a₂ to α using ha₂
  lift b₂ to α using hb₂
  norm_cast at *
  exact CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt ha hb

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply]

Goal state after:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply]
    exact hf.iterate n hx

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x

Tactic:
rw [iterate_succ_apply]

Goal state after:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x

Tactic:
rw [iterate_succ_apply]
    exact hf.iterate n hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
  by_cases hb : b = 0; · rw [hb, mul_zero, ← coe_zero, unbotD_coe, mul_zero]
  cases a; · rw [bot_mul hb, unbotD_bot, zero_mul]
  cases b; · rw [mul_bot ha, unbotD_bot, mul_zero]
  rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ a, b < f a
⊢ False

Tactic:
obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ a, b < f a
a : α
ha : m < f a
⊢ False
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬(¬IsMin a ∧ IsSuccPrelimit a) ↔ IsMin a ∨ ¬IsSuccPrelimit a

Tactic:
not_and_or,

Goal state after:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬¬IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case rfl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ a', f a < f a'
⊢ ∃ a, f a₀ < f a

Tactic:
exact h a₀

Goal state after:
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 : pred^[n + 1] b < b
⊢ f (pred^[n + 1] b) < f b

Tactic:
apply not_isMin_of_lt at hab

Goal state after:
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
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✝ : ↑s
x : α
hx : x ∈ s
h : ⟨x, hx⟩ ≤ if h : pred ↑⟨x, hx⟩ ∈ s then ⟨pred ↑⟨x, hx⟩, h⟩ else ⟨x, hx⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
dsimp at h
    split_ifs at h with h'
    · simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h
      rintro ⟨y, _⟩ hy
      simp [h hy]
    · rintro ⟨y, hy⟩ h
      rcases h.lt_or_eq with h | h
      · simp only [Subtype.mk_lt_mk] at h
        have := h.le_pred
        absurd h'
        apply out' hy hx
        simp [this, Order.pred_le]
      · simp [h]

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

Goal state before:
pp: case h
α : 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
hfat : f a ∈ t
⊢ ∀ i ∈ insert a s, ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i

Tactic:
simp_rw [mem_insert]

Goal state after:
case h
α : 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
hfat : f a ∈ t
⊢ ∀ (i : α), i = a ∨ i ∈ s → ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ γ✝ : Type u_2
x✝² : AddConst α α✝
x✝¹ : AddConst α (α✝ → β✝)
x✝ : AddConst α (β✝ → γ✝)
⊢ x✝ <*> (x✝¹ <*> x✝²) = Function.comp <$> x✝ <*> x✝¹ <*> x✝²

Tactic:
by simp [Const.map, map, Seq.seq, add_assoc]

Goal state after:
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s.powerset = univ ↔ s = univ

Tactic:
rw [← Finset.powerset_univ, powerset_inj]

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

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
s : ℕ → ↑S
hs : Surjective s
⊢ ⨆ n, (fun n ↦ ↑(s n)) n = ⊤

Tactic:
rwa [hs.iSup_comp, ← sSup_eq_iSup']

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
⊢ ↑i ≤ ↑j

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:
· assumption

Goal state after:
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
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ (v.set i a).get j = v.get j

Tactic:
by
  cases v; cases i; cases j
  simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]
  rw [List.getElem_set_of_ne]
  · simpa using h

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ : Type u
val✝ : List α✝
property✝ : val✝.length = n
⊢ id <$> ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
simp! [(· <$> ·)]

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : List α✝
property✝ : val✝.length = n
⊢ (h✝ ∘ g✝) <$> ⟨val✝, property✝⟩ = h✝ <$> g✝ <$> ⟨val✝, property✝⟩

Tactic:
simp! [(· <$> ·)]

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

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

Tactic:
exact Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬(¬IsMin (sSup s) ∧ IsSuccPrelimit (sSup s))
⊢ sSup s ∈ s

Tactic:
not_and_or,

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬¬IsMin (sSup s) ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
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:
rcases a with ((_ | _) | _) <;> rcases b with ((_ | _) | _) <;>
      simp [Equiv.sumAssoc]

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Defs

Goal state before:
pp: α : Type u_1
f g : α → α
x : α
hf : f x = x
hg : g x = x
⊢ (f ∘ g) x = x

Tactic:
comp_apply,

Goal state after:
α : Type u_1
f g : α → α
x : α
hf : f x = x
hg : g x = x
⊢ f (g x) = x
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
e : Perm α
⊢ fixedPoints ⇑(Equiv.symm e) = fixedPoints ⇑e

Tactic:
simp [Set.ext_iff]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Injective fun f ↦ f.toFun

Tactic:
rintro ⟨f, hf⟩ ⟨g, hg⟩ h
    congr with x
    exact congr_fun h x

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

Goal state before:
pp: case inl.inr
α✝ : 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
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inr b) ↔ inl a ≤ inr b

Tactic:
exact iff_of_false (@Lex.not_inr_le_inl (OrderDual β) (OrderDual α) _ _ _ _)
          Lex.not_inr_le_inl

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ x ∈ Set.range ⇑f ↔ s x b

Tactic:
hg

Goal state after:
case e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ s x b ↔ s x b
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 : α
⊢ ∀ {a' : α}, r a' a → s ↑(collapseF f a') ↑(collapseF f a)

Tactic:
change _ ∈ { b | ∀ a', r a' a → s (collapseF f a') b }

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(collapseF f a) ∈ {b | ∀ (a' : α), r a' a → s (↑(collapseF f a')) b}
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝ ≤ ⊤

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝¹, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝¹ ≤ ↑a✝

Tactic:
· simp only [Lex.sep, le_top]

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝¹, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
lt : s b ↑(collapseF f m)
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b

Tactic:
refine (collapseF_not_lt f m (fun c h ↦ ?_) lt).elim

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h✝ : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
lt : s b ↑(collapseF f m)
c : α
h : r c m
⊢ s (↑(collapseF f c)) b
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuous Prod.snd

Tactic:
simp_rw [← scottContinuousOn_univ, ScottContinuousOn.snd]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Option α
⊢ (↑o).toOption = o

Tactic:
by cases o <;> rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x

Tactic:
· assumption

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β
g : β → γ
hg : ωScottContinuous g
hf : ωScottContinuous f
⊢ ∀ (c : Chain α), (g ∘ f) (ωSup c) = ωSup (c.map { toFun := g ∘ f, monotone' := ⋯ })

Tactic:
by simp [hf.map_ωSup, hg.map_ωSup, map_comp]

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

Goal state before:
pp: ⊢ ∀ {a b c : Cardinal.{u_1}}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

Tactic:
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩

Goal state after:
case mk.mk.mk
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
· exact (power_le_power_left ha h).trans (le_max_left _ _)

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

Goal state before:
pp: case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ a, f a = b
⊢ #(Option α) ≤ #β

Tactic:
exact (f.optionElim b hb).cardinal_le

Goal state after: