mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) × α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b

Tactic:
obtain ⟨a, b, hij⟩ | ⟨a, b, hab⟩ := h

Goal state after:
case left
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r₁ i✝ j✝
⊢ Lex r₂ s₂ ⟨i✝, a⟩ ⟨j✝, b⟩

case right
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ : ι
a b : α i✝
hab : s₁ i✝ a b
⊢ Lex r₂ s₂ ⟨i✝, a⟩ ⟨i✝, b⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b → Lex r (fun i ↦ Function.swap (s i)) b a

Tactic:
· rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
      · exact Lex.left _ _ h
      · exact Lex.right _ _ h

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i ↦ Function.swap (s i)) b a → Lex (Function.swap r) s a b

Tactic:
· rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
      · exact Lex.left _ _ h
      · exact Lex.right _ _ h

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
⊢ ∀ (a b c : (i : ι) × α i), Lex r s a b → Lex r s b c → Lex r s a c

Tactic:
rintro _ _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, c, hk⟩ | ⟨_, c, hc⟩)

Goal state after:
case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝¹ : ι
a : α i✝
b : α j✝¹
hij : r i✝ j✝¹
j✝ : ι
c : α j✝
hk : r j✝¹ j✝
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
c : α j✝
hc : s j✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
j✝ : ι
c : α j✝
hk : r i✝ j✝
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨i✝, c⟩
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
argmax,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c ↦ f c < f b) none (l ++ [a]) =
    Option.casesOn (argmax f l) (some a) fun c ↦ if f c < f a then some a else some c
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
⊢ ∀ (a : α), a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l

Tactic:
a

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
⊢ a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
a₁ a₂ : Multiset α
⊢ a₁.powerset = a₂.powerset → a₁ = a₂

Tactic:
a

Goal state after:
α : Type u_1
a₁ a₂ : Multiset α
a : a₁.powerset = a₂.powerset
⊢ a₁ = a₂
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (∃ a_1 b, (a_1, b) ∈ l.sublists'.zip l.sublists'.reverse ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ a_1, (a_1, l₂) ∈ l.sublists'.zip l.sublists'.reverse ∧ a :: a_1 = l₁
⊢ l₁ ++ l₂ ~ a :: l

Tactic:
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)

Goal state after:
case cons.inl
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂' : List α
h : (l₁, l₂') ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ a :: l₂' ~ a :: l

case cons.inr
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ a :: l₁' ++ l₂ ~ a :: l
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b ↦ a \ f b) = a \ f a✝

Tactic:
inf_singleton

Goal state after:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ a \ f a✝ = a \ f a✝
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ f a✝ \ a = {a✝}.inf f \ a

Tactic:
inf_singleton

Goal state after:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ f a✝ \ a = f a✝ \ a
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
by
  rw [← iSup_univ (f := g), ← iSup_univ (f := fun i ↦ f (g i))]
  exact map_finite_biSup finite_univ f g

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

pp: case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f

Tactic:
· intro ⟨i, h⟩
    have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
    rw [this]
    refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
    simp_rw [ciSup_eq_ite]
    refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
    grind

Goal state after:
case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ a ⩿ b ↔ ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
constructor
  · intro h
    obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
    exact ⟨i, h.eval _, hi⟩
  rintro ⟨i, hab, h⟩
  refine ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hab.1) (h j · |>.1), fun c hac hcb ↦ ?_⟩
  have haci : a i < c i := by
    obtain ⟨hac, j, hj⟩ := Pi.lt_def.1 hac
    exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦
      ((lt_of_antisymmRel_of_lt (h j hj').symm hj).not_ge (hcb.le j)).elim
  have hcbi : c i < b i := by
    obtain ⟨hcb, j, hj⟩ := Pi.lt_def.1 hcb
    exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦
      ((lt_of_lt_of_antisymmRel hj (h j hj').symm).not_ge (hac.le j)).elim
  exact hab.2 haci hcbi

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
obtain ⟨a, ha⟩ := hs.exists_maximal hn

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
⊢ Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, mem_range_self x⟩, ?_⟩⟩
  · rw [← f.le_iff_le, ← f.le_iff_le]
    exact h.le_of_le ⟨hy, mem_range_self y⟩
  rintro _ ⟨hyt, ⟨y, rfl⟩⟩
  simp_rw [f.le_iff_le]
  exact h.le_of_le hyt

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range ⇑f
⊢ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
by
  rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
a b : α
⊢ b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a

Tactic:
h₀_finset_mem_Ioi,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
a b : α
⊢ a < b ↔ b ∈ h₁_finset_Ioi a
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
  · refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
    obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
    induction x with
    | zero => apply hr
    | succ x ih =>
      apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
  · exact ⟨g, Or.intro_right _ hnr⟩

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
· obtain h := WellFoundedGT.monotone_chain_condition a
    exact (Nat.sInf_mem (s := {n | ∀ m, n ≤ m → a n = a m}) h m hm.le).ge

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ), ¬IsMax (a n) → a n ⋖ a (n + 1)
⊢ ∃ n, IsMax (a n)

Tactic:
by_contra!

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ), ¬IsMax (a n) → a n ⋖ a (n + 1)
this : ∀ (n : ℕ), ¬IsMax (a n)
⊢ False
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
simp_rw [Finset.range_eq_Ico, map_eq_image]

Goal state after:
a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a)) (Ico 0 b)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
⊢ P x

Tactic:
by
  let Q : s → Prop := fun y => P y
  change Q ⟨x, hx⟩
  refine WellFounded.induction hs ⟨x, hx⟩ ?_
  simpa only [Subtype.forall]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ 0 = 0 - 1

Tactic:
Nat.zero_sub

Goal state after:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ 0 = 0
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ 0 = 0 - 1

Tactic:
Nat.zero_sub

Goal state after:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ 0 = 0
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ x✝ • (a✝ * b✝) = a✝ * b✝

Tactic:
by rw [smul_mul', ha, hb]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a₁ a₂ : α
⊢ a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁

Tactic:
by
  simp_rw [← orbit_eq_iff, eq_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs m) m) (↑(fs n) n)

Tactic:
h m n mn.le

Goal state after:
case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs n) m) (↑(fs n) n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r ((fun n ↦ ↑(fs n) n) m) ((fun n ↦ ↑(fs n) n) n)

Tactic:
dsimp
    rw [h m n mn.le]
    exact (fs n).2.1.2 m n mn

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
⊢ False

Tactic:
apply hf1.2 m n mn
    rwa [if_pos hn, if_pos (mn.trans hn)] at hmn

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n

Tactic:
use (g 0), (g n)

Goal state after:
case h
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ g 0 < g n ∧ f (g 0) ≤ f (g n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ s.WellFoundedOn (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩)

Tactic:
by
  change WellFounded (Sigma.Lex rι rπ on fun c : s => ⟨f c, g (f c) c⟩)
  exact
    @WellFounded.sigma_lex_of_wellFoundedOn_fiber _ s _ _ rπ (fun c => f c) (fun i c => g _ c) hι
      fun i => ((hπ i).onFun (f := fun x => ⟨x, x.1.2, x.2⟩)).mono (fun b c h => ‹_›)

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 : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ (∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z) ∧ y * z ∈ ↑C

Tactic:
refine ⟨?_, mul_mem (h hy) hzC⟩

Goal state after:
case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ ∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a

Tactic:
by
  convert! @disjoint_sum_left _ a (map f i.val)
  simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ f a = if p a then f a else 1

Tactic:
rw [if_pos]; simpa using (mem_filter.1 h).2

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

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ {a} ⊆ s

Tactic:
intro _ H
          rwa [mem_singleton.1 H]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ Subsingleton (G ⧸ N) ↔ N = ⊤

Tactic:
by
  simp [HasQuotient.Quotient]

Goal state after:
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
h : ∀ a ∈ s, f a = 1
⊢ ∏ x ∈ s, f x = 1

Tactic:
exact prod_eq_one h

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ (List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)

Tactic:
simp only [List.map, List.prod_cons, toFinset_cons, IH]
  by_cases has : a ∈ s.toFinset
  · rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
    congr 1
    refine prod_congr rfl fun x hx => ?_
    rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
  rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
  grind [Finset.prod_congr]

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 : ι → ℕ
a : M
x✝³ : ι
x✝² : Finset ι
x✝¹ : x✝³ ∉ x✝²
x✝ : ∏ i ∈ x✝², a ^ f i = a ^ ∑ i ∈ x✝², f i
⊢ ∏ i ∈ cons x✝³ x✝² x✝¹, a ^ f i = a ^ ∑ i ∈ cons x✝³ x✝² x✝¹, f i

Tactic:
by simp [prod_cons, sum_cons, pow_add, *]

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
⊢ (_root_.Disjoint on t') i j

Tactic:
a

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 ι
⊢ a ⊆ t' i → a ⊆ t' j → a ⊆ ⊥
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker

Tactic:
codisjoint_iff,

Goal state after:
case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⊤ ⊔ f.ker = ⊤
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker

Tactic:
codisjoint_iff,

Goal state after:
case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⊤ ⊔ f.ker = ⊤
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ N ⊔ Subgroup.map H.subtype ⊤ = ⊤ ⊔ N

Tactic:
← hHN,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ N ⊔ Subgroup.map H.subtype ⊤ = N ⊔ H ⊔ N
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
⊢ (r₁ /ₒ s₁ * y) • z = (r₁ /ₒ s₁) • y • z

Tactic:
cases y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • z = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • z