mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
⊢ ⇑(r.map f) = Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2

Tactic:
by
  refine le_antisymm ?_ (sup_le Relation.EqvGen.rel (by rintro _ _ rfl; exact .refl _))
  rintro _ _ hxy
  induction hxy with
  | rel _ _ hab => exact .inl hab
  | refl _ => exact .inr rfl
  | symm _ _ _ ih => exact ih.imp (Std.Symm.symm _ _) (Std.Symm.symm _ _)
  | trans _ _ _ _ _ ih1 ih2 =>
    rcases ih1 with ih1 | rfl
    · rcases ih2 with ih2 | rfl
      · exact .inl <| r.iseqv.isTrans.map hf |>.trans _ _ _ ih1 ih2
      · exact .inl ih1
    · exact ih2

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x✝ y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x✝ = ↑y
x : M
⊢ ↑(f (f x)) * ↑(f x) * (↑x * ↑(f x)) = ↑(f (f x)) * (↑(f x) * ↑x) * ↑(f x)

Tactic:
by simp_rw [mul_assoc]

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

Goal state before:
pp: α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
⊢ Red L₃ [(x1, !b1), (x2, b2)]

Tactic:
have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red

Goal state after:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
⊢ Red L₃ [(x1, !b1), (x2, b2)]
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → x ∉ {x ∈ s | p x} → f x = 1

Tactic:
rw [not_imp_comm, mem_filter]

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red.Step L₁ L₂
⊢ Join (ReflTransGen Red.Step) L₁ L₂

Tactic:
exact le_join_of_refl L₁ L₂ h.to_red

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∏ x ∈ s, f x = ∏ x ∈ t, g x

Tactic:
classical
  calc
    ∏ x ∈ s, f x = ∏ x ∈ s with f x ≠ 1, f x := by rw [prod_filter_ne_one]
    _ = ∏ x ∈ t with g x ≠ 1, g x :=
      prod_bij (fun a ha => i a (mem_filter.mp ha).1 <| by simpa using (mem_filter.mp ha).2)
        ?_ ?_ ?_ ?_
    _ = ∏ x ∈ t, g x := prod_filter_ne_one _
  · grind
  · solve_by_elim
  · intro b hb
    refine (mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_
    obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂
    exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩
  · solve_by_elim

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
hij : i ≠ j
a : Finset ι
hai : a ⊆ t' i
haj : a ⊆ t' j
k : ι
hk : k ∈ a
hki : k ∈ t' i
hkj : k ∈ t' j
⊢ k ∈ ⊥

Tactic:
simp only [ne_eq, mem_filter, t'] at hki hkj

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
hij : i ≠ j
a : Finset ι
hai : a ⊆ t' i
haj : a ⊆ t' j
k : ι
hk : k ∈ a
hki : k ∈ t i ∧ ¬f k = 1
hkj : k ∈ t j ∧ ¬f k = 1
⊢ k ∈ ⊥
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
intro p

Goal state after:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
⊢ p ∈ H₁ → ∀ g₂ ∈ H₂, ⁅f p, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
⊢ (map id) x = x

Tactic:
map_id,

Goal state after:
α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
⊢ (AddMonoidHom.id (FreeAbelianGroup α)) x = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
⊢ (map id) x = x

Tactic:
map_id,

Goal state after:
α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
⊢ (AddMonoidHom.id (FreeAbelianGroup β)) x = x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:

Tactic:
(t₂ * t₁ : M) * (b.2 * d.2 * (a.1 * c.1)) = t₂ * (d.2 * c.1) * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = (t₂ * t₁ : M) * (a.2 * c.2 * (b.1 * d.1)) := by rw [ht₁, ht₂]; ac_rfl

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : Group α
inst✝ : Preorder α
a b : (WithZero α)ˣ
⊢ WithZero.unitsWithZeroEquiv.toFun a ≤ WithZero.unitsWithZeroEquiv.toFun b ↔ a ≤ b

Tactic:
simp [WithZero.unitsWithZeroEquiv]

Goal state after:
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⟩

Tactic:
← mul_one (oreDenom (c • 1) _),

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⟩ * 1)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n

Tactic:
cases n with
  | zero => exact h₀
  | succ n =>
    refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;>
    exact hk.trans n.succ.lt_succ_self

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : α
hab : ↑a ≤ ⊥
⊢ (↑a).succ ≤ ⊥.succ

Tactic:
simp at hab

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : α
hab : ⊤ ≤ ↑a
⊢ ⊤.pred ≤ (↑a).pred

Tactic:
simp at hab

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ^[n + 1] m) hmn

Tactic:
Function.iterate_succ_apply'

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ (Order.succ^[n] m)) ⋯
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ Ioo a b = ∅ ↔ b ≤ succ a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : Ioo a b = ∅
⊢ b ≤ succ a

case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
⊢ Ioo a b = ∅
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : IsMax a
⊢ SuccOrder.succ a = SuccOrder.succ a

pp: case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ SuccOrder.succ a = SuccOrder.succ a

Tactic:
· exact (@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ SuccOrder.succ a = SuccOrder.succ a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg.h
α : 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
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩

Tactic:
exact this

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✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ^[n + 1] a ∈ s
⊢ f a ≤ f (succ^[n + 1] a)

Tactic:
Function.iterate_succ_apply'

Goal state after:
case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
⊢ f a ≤ f (succ (succ^[n] a))
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hb : succ^[0] a ∈ s
hab : a < succ^[0] a
⊢ f a < f (succ^[0] a)

Tactic:
simp at hab

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

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

Tactic:
Function.iterate_succ_apply'

Goal state after:
case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
⊢ f a < f (succ (succ^[n + 1] a))
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 : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred^[n + 1] b ∈ s
⊢ f (pred^[n + 1] b) ≤ f b

Tactic:
Function.iterate_succ_apply'

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 : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
⊢ f (pred (pred^[n] b)) ≤ f b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case zero
α : 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
ha : pred^[0] b ∈ s
hab : pred^[0] b < b
⊢ f (pred^[0] b) < f b

Tactic:
simp at hab

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

Goal state before:
pp: case succ.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
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred^[n + 1 + 1] b ∈ s
⊢ f (pred^[n + 1 + 1] b) < f b

Tactic:
Function.iterate_succ_apply'

Goal state after:
case succ.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
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using! hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using! hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using! hi

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
⊢ map (⇑e) (map (⇑e.symm) x) = x

Tactic:
rw [map_map, Equiv.self_comp_symm, map_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (filter (fun x ↦ a ≠ x) ↑m).card + ↑⟨count a ↑m, ⋯⟩ = (↑m).card

Tactic:
rw [← countP_eq_card_filter, add_comm]

Goal state after:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑⟨count a ↑m, ⋯⟩ + countP (fun x ↦ a ≠ x) ↑m = (↑m).card
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m

pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
· rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.nil
α : 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
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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (n + 1)
w : Vector γ (n + 1)
u_property : [].length = n + 1
⊢ C ⟨[], u_property⟩ v w

pp: case succ.cons
α : 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
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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (n + 1)
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
⊢ C ⟨a :: u, u_property⟩ v w

Tactic:
cases u_property

Goal state after:
case succ.cons
α : 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
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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (n + 1)
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
⊢ C ⟨a :: u, u_property⟩ v w
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
xs : Vector α n
⊢ xs ++ nil = xs

Tactic:
cases xs

Goal state after:
case mk
α : Type u_1
n : ℕ
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨val✝, property✝⟩ ++ nil = ⟨val✝, property✝⟩
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

pp: case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
· simpa using trans_trichotomous_right ha hb

Goal state after:
case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
⊢ Std.Trichotomous (Lex r s)

Tactic:
by
  grind [Std.Trichotomous, Lex]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
⊢ ∃ b, a < b

Tactic:
obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)
        · exact ⟨b, inl_lt_inl_iff.1 h⟩
        · exact (not_inl_lt_inr h).elim

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

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
by
  simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
⊢ Injective toRelEmbedding

Tactic:
rintro ⟨f, a, hf⟩ ⟨g, b, hg⟩ rfl

Goal state after:
α : 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
⊢ { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf } =
    { toRelEmbedding := { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding, top := b,
      mem_range_iff_rel' := hg }
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a b : WithTop α
⊢ ((Equiv.optionEquivSumPUnit α).trans toLex) a ≤ ((Equiv.optionEquivSumPUnit α).trans toLex) b ↔ a ≤ b

Tactic:
simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Lex.toLex_le_toLex, le_refl]
    cases a <;> cases b
    · simp only [lex_inr_inr, le_top]
    · simp only [lex_inr_inl, false_iff]
      exact not_top_le_coe _
    · simp only [Lex.sep, le_top]
    · simp only [lex_inl_inl, coe_le_coe]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b ≤ f a ↔ ∃ c ≤ a, f c = b

Tactic:
constructor
  · intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_le h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.le_iff_le] at h
  · rintro ⟨c, hc, rfl⟩
    exact f.monotone hc

Goal state after: