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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)

pp: case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Tactic:
· constructor
    · simp_rw [sigmaLift]
      simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
        and_imp]
      rintro x hx rfl
      exact ⟨rfl, rfl, hx⟩
    · rintro ⟨⟨⟩, ⟨⟩, hx⟩
      rw [sigmaLift, dif_pos rfl, mem_map]
      exact ⟨_, hx, by simp⟩

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x ↦ P x ∧ Q x) x ↔ Minimal P x ∧ Q x

Tactic:
and_iff_left_of_imp (fun x ↦ hPQ x),

Goal state after:
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x ↦ P x) x ↔ Minimal P x ∧ Q x
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
⊢ Q x

pp: case refine_2
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y

Tactic:
· obtain ⟨y, hyx, hy⟩ := h h'.prop
    rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]

Goal state after:
case refine_2
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
rintro ⟨x, (hx : Minimal _ x), rfl⟩

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : α
hx : Minimal P x
⊢ f x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

pp: case refine_2
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ x ∈ f '' {x | Minimal P x}

Tactic:
· rintro ⟨x, (hx : Minimal _ x), rfl⟩
    exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ x ∈ f '' {x | Minimal P x}
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b

Tactic:
rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_ge, lt_iff_le_not_ge]

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_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
a b x : α
⊢ x ∈ h₀_finset_Ioc a b ↔ x ∈ h₁_finset_Ioc a b

Tactic:
h₀_finset_mem_Ioc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
a b x : α
⊢ a < x ∧ x ≤ b ↔ x ∈ h₁_finset_Ioc a b
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬a n < a m ↔ a n = a m

Tactic:
rw [lt_iff_le_and_ne]

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬(a n ≤ a m ∧ a n ≠ a m) ↔ a n = a m
Module: Mathlib.Order.OrderIsoNat

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

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

Tactic:
· exact a.monotone hm

Goal state after:
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ a m ≤ monotonicSequenceLimit a
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
m n : ℕ
hlt : m < n
hle : r ((f ∘ ⇑g) m) ((f ∘ ⇑g) n)
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
cases h2 m n hlt hle

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
⊢ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
WellFounded.wellFounded_iff_has_min

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
⊢ ∀ (s_1 : Set α), s_1.Nonempty → ∃ m ∈ s_1, ∀ x ∈ s_1, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = insert b (Ico a b)

Tactic:
Ico_insert_right h

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (Ici a).erase a ↔ a✝ ∈ Ioi a

Tactic:
Finset.mem_erase,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ≠ a ∧ a✝ ∈ Ici a ↔ a✝ ∈ Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ (Iic b).erase b ↔ a✝ ∈ Iio b

Tactic:
Finset.mem_erase,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ≠ b ∧ a✝ ∈ Iic b ↔ a✝ ∈ Iio b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → c ∉ [[a, b]]

Tactic:
by
  rw [mem_uIcc]
  exact Set.notMem_uIcc_of_gt

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 α
x : α
⊢ x ∈ Set.univ ↔ x ∈ ⋃ x, x.orbit

Tactic:
simp only [Set.mem_univ, Set.mem_iUnion, true_iff]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ ∃ i, x ∈ i.orbit
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * z * c = a * (c * z)

Tactic:
← h.right_assoc,

Goal state after:
M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * z * c = a * c * z
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst = ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
· dsimp only [InvImage, (· on ·)] at h' ⊢
    convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1; swap
    · exact ⟨c, h'⟩
    · exact PSigma.subtype_ext (Subtype.ext h') rfl
    · dsimp only [Subtype.coe_mk, Subrel, Order.Preimage] at *
      grind

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
x : G
⊢ closure {x}⁻¹ = closure {x}

Tactic:
closure_inv

Goal state after:
G : Type u_2
inst✝ : Group G
x : G
⊢ closure {x} = closure {x}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mem
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ i, ↑(S i)
⊢ C x

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ (List.map f s.toList).prod = s.prod f

Tactic:
by
  rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Set M
n : M → ℕ
t : Finset M
hts : ↑t ⊆ s
⊢ ∏ a ∈ t, a ^ n a ∈ closure s

Tactic:
exact prod_mem _ fun x hx ↦ pow_mem (subset_closure <| hts hx) _

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
s : Finset G
⊢ Subgroup.closure (⇑(Subgroup.closure ↑s).subtype ⁻¹' ↑s) = ⊤

Tactic:
Subgroup.closure_preimage_eq_top

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ ⊤ = ⊤
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
by_cases hy₃ : Minimal (· ∈ { x | x ∈ P ∧ x ≠ 1 }) y

Goal state after:
case pos
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

case neg
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≠ 1

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y

Tactic:
· exact (one_lt_of_lt_mul_right hz₁).ne.symm

Goal state after:
case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ id <$> (-pure x) = -pure x

Tactic:
by rw [FreeAbelianGroup.map_neg, ih]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y : FreeAbelianGroup α
⊢ (lift ⇑f) (x * y) = (lift ⇑f) x * (lift ⇑f) y

Tactic:
by
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, map_zero]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul, map_zero]
        | of L1 =>
          simp_rw [of_mul_of, lift_apply_of]
          exact f.map_mul _ _
        | neg L1 ih =>
          simp_rw [neg_mul, map_neg, neg_mul]
          exact congr_arg Neg.neg ih
        | add x1 x2 ih1 ih2 => simp only [add_mul, map_add, ih1, ih2]
      | neg L2 ih => rw [mul_neg, map_neg, map_neg, mul_neg, ih]
      | add y1 y2 ih1 ih2 => rw [mul_add, map_add, map_add, mul_add, ih1, ih2]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
⊢ v₀ • r₂ /ₒ (u₀ * s₁) = v • r₂ /ₒ (u * s₁)

Tactic:
rcases ore_right_cancel _ _ _ this with ⟨s₄, hs₄⟩

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ v₀ • r₂ /ₒ (u₀ * s₁) = v • r₂ /ₒ (u * s₁)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
x : OreLocalization S X
⊢ 1 • x = x

Tactic:
cases x with | _ r s
  simp [OreLocalization.one_def, oreDiv_smul_char 1 r 1 s 1 s (by simp)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Tactic:
induction a <;> induction b

Goal state after:
case top.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∧ ⊤ ≠ ⊤

case top.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∧ ↑a✝ ≠ ⊤

case coe.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∧ ⊤ ≠ ⊤

case coe.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∧ ↑a✝ ≠ ⊤
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
R : Type ?u.51
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : IsScalarTower R M M
inst✝¹ : MulAction R X
inst✝ : IsScalarTower R M X
s₁ s₂ : R
x : OreLocalization S X
⊢ (s₁ • s₂) • x = s₁ • s₂ • x

Tactic:
smul_assoc

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
R : Type ?u.51
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : IsScalarTower R M M
inst✝¹ : MulAction R X
inst✝ : IsScalarTower R M X
s₁ s₂ : R
x : OreLocalization S X
⊢ s₁ • s₂ • x = s₁ • s₂ • x
Module: Mathlib.Order.Iterate

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

Tactic:
by
  cases n
  exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
⊢ IsMax (succ^[n] a)

Tactic:
rcases le_total n m with h | h
  · exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)
  · rw [h_eq]
    exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
⊢ succ a < b

Tactic:
by
  by_cases h : IsMax a
  · rwa [h.succ_eq]
  · rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
    refine ⟨ha, fun hab => ?_⟩
    subst hab
    exact (h hb.isMax).elim

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
⊢ x = x - 0

Tactic:
sub_zero

Goal state after:
case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
⊢ x = x
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
⊢ motive a

Tactic:
by
  have A : ∀ n : ℕ, motive n := fun n => Nat.recOn n zero succ
  cases a
  · exact top A
  · exact A _

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
y : F α
⊢ (fun {α} ↦ η.app α) (x <$> y) = x <$> (fun {α} ↦ η.app α) y

Tactic:
rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
g : (a : α) → π a → ℕ
hg : ∀ (a : α), Injective (g a)
⊢ Countable (Sigma π)

Tactic:
exact ((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable

Goal state after: