mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
a : δ i
ha : a ∈ s i
⊢ piFinset (update s i {a}) = {f ∈ piFinset s | f i = a}

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x

Tactic:
exact ⟨y_in, fun j _ => by simpa using hz j⟩

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ op '' s⁻¹ = (op '' s)⁻¹

Tactic:
by
  simp_rw [← image_inv_eq_inv, Function.Semiconj.set_image op_inv s]

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

Goal state before:
pp: case a.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x ∈ ↑(closure s)

Tactic:
exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ 1 ∈ Set.ofPred IsUnit

Tactic:
simp only [isUnit_one, Set.mem_ofPred_eq]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ y⁻¹ * x ∈ f.ker

Tactic:
rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ map f H = map f K ↔ H ⊔ f.ker = K ⊔ f.ker

Tactic:
by simp only [le_antisymm_iff, map_le_map_iff']

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : map f H = map f K
⊢ H = K

Tactic:
by
  apply_fun comap f at hf
  rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
constructor
  · intro h
    constructor
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

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

Goal state before:
pp: motive : ℕ → Sort u
H₁ : (b : Bool) → (n : ℕ) → motive (bit b n)
⊢ ∀ ⦃a₂ : (b : Bool) → (n : ℕ) → motive (bit b n)⦄,
    (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) a₂ → H₁ = a₂

Tactic:
H₂

Goal state after:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
⊢ (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂ → H₁ = H₂
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
x✝ : Set β
⊢ 1 • x✝ = x✝

Tactic:
by simp only [← image_smul, one_smul, image_id']

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ a • A ⊆ B ↔ A ⊆ a⁻¹ • B

Tactic:
refine image_subset_iff.trans ?_
  congr! 1
  exact ((MulAction.toPerm _).image_symm_eq_preimage _).symm

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ g (f_inv (x * y)) * (g (f_inv x * f_inv y))⁻¹ = 1

Tactic:
← g.map_inv,

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ g (f_inv (x * y)) * g (f_inv x * f_inv y)⁻¹ = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x)) * (g x)⁻¹ = 1

Tactic:
← g.map_inv,

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x)) * g x⁻¹ = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set N
f : G ≃* N
⊢ normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)

Tactic:
have := f.toEquiv.image_symm_eq_preimage s

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set N
f : G ≃* N
this : ⇑f.symm '' s = ⇑f.toEquiv ⁻¹' s
⊢ normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case hS
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ S ↑x

Tactic:
← Function.comp_def,

Goal state after:
case hS
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) (S ∘ Subtype.val)
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
· obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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

Goal state before:
pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
· obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ inl a ∈ s.disjSum t ↔ a ∈ s

Tactic:
rw [mem_disjSum, or_iff_left]
  · simp only [inl.injEq, exists_eq_right]
  rintro ⟨b, _, hb⟩
  exact inr_ne_inl hb

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f : TopHom β γ
g : TopHom α β
⊢ f ⊤ = ⊤

Tactic:
map_top

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f : TopHom β γ
g : TopHom α β
⊢ ⊤ = ⊤
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).max ≠ ↑x

Tactic:
by_cases! s0 : (s.erase x).Nonempty
  · refine ne_of_eq_of_ne (coe_max' s0).symm ?_
    exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)
  · rw [s0, max_empty]
    exact WithBot.bot_ne_coe

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ powersetCard n ⟦l⟧ ≤ powerset ⟦l⟧

Tactic:
by
    simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]
    exact ((sublistsLen_sublist_sublists' _ _).map _).subperm

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset

Tactic:
simp only [mem_powerset, mem_image, mem_union, subset_insert_iff]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
hxt : x ⊆ t
hxn : #x = n
hsx : s ⊆ x
⊢ ∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x

Tactic:
exact ⟨x \ s, ⟨fun y hy => mem_sdiff.mpr ⟨hxt (mem_sdiff.mp hy).1, (mem_sdiff.mp hy).2⟩,
           by rw [card_sdiff_of_subset hsx, hxn]⟩, sdiff_union_of_subset hsx⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ powersetCard 0 s = {∅}

Tactic:
by
  grind

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | f x ∈ t}) = t
⊢ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
refine ⟨_, ?_, this⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | f x ∈ t}) = t
⊢ {x ∈ s | f x ∈ t} ⊆ s ∧ #({x ∈ s | f x ∈ t}) = n
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
rw [image_eq_range] at hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (range fun x ↦ f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
⊢ iSup f ⊔ iSup g ≤ ⨆ x, f x ⊔ g x

Tactic:
have := bbdAbove_range_sup Hf Hg

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
this : BddAbove (range fun x ↦ f x ⊔ g x)
⊢ iSup f ⊔ iSup g ≤ ⨆ x, f x ⊔ g x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
by_cases hq : q

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
by_cases hq : q

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i ↦ t₁ i ∩ t₂ i

Tactic:
by
  grind

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
by_cases hq : q

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
by_cases hq : q

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (⨆ i, f i) = ⨆ i, l (f i)

Tactic:
by rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
rw [image_eq_range] at hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (range fun x ↦ f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ f y ≤ f x → f x ≤ f y

Tactic:
hf hx.prop hy,

Goal state after:
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ f y ≤ f x → x ≤ y
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ Iio a = range a

Tactic:
by
  grind

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ range n = Icc 0 (n - 1)

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
m n : ℕ
mn : m < n
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad) m)) (f ((Nat.orderEmbeddingOfSet bad) n))

Tactic:
have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
m n : ℕ
mn : m < n
h : (Nat.orderEmbeddingOfSet bad) m ∈ Set.range ⇑(Nat.orderEmbeddingOfSet bad)
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad) m)) (f ((Nat.orderEmbeddingOfSet bad) n))
Module: Mathlib.Order.OrderIsoNat

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

Tactic:
refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m n : ℕ
mn : m < n
⊢ r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ x ∈ image (⇑(addLeftEmbedding a)) (Ico 0 b) ↔ x ∈ Ico a (a + b)

Tactic:
simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]

Goal state after:
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ {x ∈ Ico a b | x < c} = Ico a c

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ {x ∈ Ico a b | c ≤ x} = Ico c b

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inl
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), ↑(f (g n)) ∈ s
m n : ℕ
hlt : m < n
hr : r ↑(f (g m)) ↑(f (g n))
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono hlt, hr⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), ↑(f (g n)) ∈ t
m n : ℕ
hlt : m < n
hr : r ↑(f (g m)) ↑(f (g n))
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono hlt, hr⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ {x ∈ Ico a b | x ≤ a} = {a}

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
by
  by_cases h : a < b
  · rw [Ico_eq_cons_Ioo h, card_cons]
    exact (Nat.add_sub_cancel _ _).symm
  · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic b \ Ioc a b = Iic (min a b)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iic a ∪ Ioc a b = Iic b

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : 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
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
have h : ∀ m n, m ≤ n → (fs m).1 m = (fs n).1 m := fun m n mn => by
    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le mn; clear mn
    induction k with
    | zero => rfl
    | succ k ih =>
      rw [ih, (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
        (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]
      rfl

Goal state after:
α : 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
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
by
  simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g ∈ normalizer ↑H

Tactic:
← (normalizer H : Subgroup G).inv_mem_iff

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g⁻¹ ∈ normalizer ↑H
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case of
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x y : M), r x y → s x y

pp: case refl
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x : M), s x x

pp: case symm
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → s x y → s y x

pp: case trans
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → s x y → s y z → s x z

pp: case mul
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → s w x → s y z → s (w * y) (x * z)

Tactic:
· exact fun x y h => hs x y h

Goal state after:
case refl
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x : M), s x x

case symm
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → s x y → s y x

case trans
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → s x y → s y z → s x z

case mul
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → s w x → s y z → s (w * y) (x * z)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
a : α
b : Bool
⊢ ¬Step [(a, b)] L

Tactic:
simp [Step.cons_left_iff, not_step_nil]

Goal state after: