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

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)

Tactic:
Fin.append_right,

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ x i = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case intro
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
⊢ WellFounded r

Tactic:
have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [lt_iff_le_not_ge, Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩

Goal state after:
case intro
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
this : ∀ (x y : α), r x y → #{z | r z x} < #{z | r z y}
⊢ WellFounded r
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inl
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
a : α
hs : {a}.Nonempty
⊢ p {a} hs

Tactic:
exact h₀ _

Goal state after:
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ y :: l₁✝
⊢ x ∈+ y :: l₂✝

Tactic:
rw [duplicate_cons_iff] at hx ⊢

Goal state after:
case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : y = x ∧ x ∈ l₁✝ ∨ x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l✝ : List α
x✝ : α
inst✝ : DecidableEq α
x y : α
l : List α
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hx : ¬(y = x ∧ x ∈ l)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simpa [duplicate_cons_iff, h] using hx

Goal state after:
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
xs : List α
hx : ¬x ∈ xs
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
by
  induction xs <;> grind

Goal state after:
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ orderedInsert r x xs

Tactic:
by
  induction xs <;> grind

Goal state after:
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
as bs : List α
x : α
hs : as <+ bs
hb : Pairwise r bs
⊢ orderedInsert r x as <+ orderedInsert r x bs

Tactic:
cases as with

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ i.removeNth (j.removeNth m) ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m)

Tactic:
apply Function.hfunext rfl
  simp only [heq_iff_eq]
  rintro k _ rfl
  unfold removeNth
  apply congr_arg_heq
  rw [succAbove_succAbove_succAbove_predAbove]

Goal state after:
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → Pairwise R (a :: b :: l)

Tactic:
simp_rw [pairwise_cons_cons_iff_of_trans]

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → R a b ∧ Pairwise R (b :: l)
Module: Mathlib.Data.List.Range

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
rw [isChain_range, succ_eq_add_one, Nat.add_one_sub_one]

Goal state after:
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c : α
⊢ ∀ {c_1 : α},
    r c c_1 →
      Relation.ReflTransGen r c_1 b →
        (∃ l, IsChain r (c_1 :: l) ∧ (c_1 :: l).getLast ⋯ = b) → ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
d

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
⊢ r c d →
    Relation.ReflTransGen r d b →
      (∃ l, IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b) → ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ a > b

Tactic:
cases as with

Goal state after:
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ (l.rotate n)[k]? = l[(k + n) % l.length]?

Tactic:
getElem?_rotate

Goal state after:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ l[(k + n) % l.length]? = l[(k + n) % l.length]?

α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n

Tactic:
refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩
    refine (Nat.mod_lt _ ?_).le
    simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ n.choose k + n.choose k.succ = 0

Tactic:
choose_eq_zero_of_lt hnk,

Goal state after:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ 0 + n.choose k.succ = 0
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
h₁ : a'' ≠ a
b' : δ a''
h : a ≠ a''
ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m
ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
⊢ cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂

pp: case inl.inr
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : ha₁ ≍ ha₂
⊢ cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁ ≍ cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂

Tactic:
all_goals simp [*, Pi.cons_same, Pi.cons_ne]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝² x✝¹ : N
x✝ : α
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by simpa [(· • ·)] using mul_smul ..

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ a = b

Tactic:
by
    rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc
    exact hc

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ ∀ (a : α), ConjClasses.mk (Quotient.lift id ⋯ (ConjClasses.mk a)) = ConjClasses.mk a

Tactic:
solve_by_elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
⊢ SurjOn f (⋂ i, s i) t

Tactic:
intro y hy
  rw [Hinj.image_iInter_eq, mem_iInter]
  exact fun i => H i hy

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

Goal state before:
pp: case rs
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n

Tactic:
gcongr

Goal state after:
case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case rt
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n

Tactic:
gcongr

Goal state after:
case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
⊢ t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Tactic:
by
  rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
⊢ ⇑m ⁻¹' s / ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s / t)

Tactic:
rintro _ ⟨_, _, _, _, rfl⟩
  exact ⟨_, ‹_›, _, ‹_›, (map_div m ..).symm⟩

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.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
by
        simp [← mul_assoc, h₁, h₂]

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

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
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
g : N →* G
h : LeftInverse ⇑g ⇑f
y : G
⊢ f.rangeRestrict ((⇑g ∘ ⇑f.range.subtype) ⟨f y, ⋯⟩) = ⟨f y, ⋯⟩

Tactic:
solve_by_elim

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
hf : Surjective ⇑f
H : Subgroup N
⊢ comap f H = f.ker ↔ H = ⊥

Tactic:
rw [comap_eq_ker, f.range_eq_top_of_surjective hf, disjoint_top]

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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
by
  simp_rw [closure, op_sInf, Set.preimage_ofPred_eq, Submonoid.coe_unop]
  congr with a
  exact MulOpposite.unop_surjective.forall

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ normalizer ↑H = (normalizer ↑H.unop).op

Tactic:
op_normalizer,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ normalizer ↑H = normalizer ↑H.unop.op
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n - n.sqrt * n.sqrt, n.sqrt).1 (n - n.sqrt * n.sqrt, n.sqrt).2 = n

Tactic:
simp [s, pair, h, sm]

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

Goal state before:
pp: n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ binaryRec [] (fun b x IH ↦ b :: IH) (bit b n) = b :: binaryRec [] (fun b x IH ↦ b :: IH) n

Tactic:
binaryRec_eq

Goal state after:
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ b :: binaryRec [] (fun b x IH ↦ b :: IH) n = b :: binaryRec [] (fun b x IH ↦ b :: IH) n

case h
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: m n : ℕ
⊢ max m n ^ 2 + min m n ≤ pair m n

Tactic:
rw [pair]

Goal state after:
m n : ℕ
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
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
H K✝ : Subgroup G
inst✝ : H.Characteristic
K : Subgroup ↥H
hK : K.Characteristic
⊢ (map H.subtype K).Characteristic

Tactic:
refine characteristic_iff_map_eq.2 fun φ ↦ ?_
  have := congr_arg (map H.subtype) <| characteristic_iff_map_eq.1 hK (MulAut.characteristic H φ)
  simpa [Subgroup.map_map, MulAut.characteristic]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
⊢ Function.Surjective f

Tactic:
d

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
⊢ ∃ a, f a = d
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ⊆ z • s⁻¹ * s

case h₂
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b • t ⊆ z • t⁻¹ * t
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ Function.Surjective ⇑(map f)

Tactic:
d

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
d : FreeMonoid β
⊢ ∃ a, (map f) a = d
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
have hp_a : p a := hl a mem_cons_self

Goal state after:
case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
hp_a : p a
⊢ f (a * l.prod) ≤ f a * (map f l).prod
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⟩)
    · exact Lex.left _ _ (_root_.trans hij hk)
    · exact Lex.left _ _ hij
    · exact Lex.left _ _ hk
    · exact Lex.right _ _ (_root_.trans hab hc)

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ motive x

Tactic:
exact mem _ _ hi

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ x ≤ y

Tactic:
rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left]

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    (l'.sublists ++ map (fun x ↦ x ++ [a]) l'.sublists).zip
      ((map (fun x ↦ x ++ [a]) l'.sublists).reverse ++ l'.sublists.reverse)
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
zip_append (by simp),

Goal state after:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    l'.sublists.zip (map (fun x ↦ x ++ [a]) l'.sublists).reverse ++
      (map (fun x ↦ x ++ [a]) l'.sublists).zip l'.sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
o : Option α
⊢ o.toFinset.card = o.elim 0 1

Tactic:
cases o <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
powersetCard_eq_filter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ {x ∈ (insert x s).powerset | #x = n.succ} = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
this : insert a i = insert a j → i = j
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
aesop (add simp [Set.Nonempty, Set.subset_def])

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f

Tactic:
· exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ ↑(s.sup' H f) ≤ ↑a ↔ ∀ b ∈ s, ↑(f b) ≤ ↑a

Tactic:
coe_sup',

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ s.sup (WithBot.some ∘ f) ≤ ↑a ↔ ∀ b ∈ s, ↑(f b) ≤ ↑a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ ↑((map f s).sup' hs g) = ↑(s.sup' ⋯ (g ∘ ⇑f))

Tactic:
coe_sup',

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ (map f s).sup (WithBot.some ∘ g) = ↑(s.sup' ⋯ (g ∘ ⇑f))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑a ≤ ↑(s.sup' H f) ↔ ∃ b ∈ s, a ≤ f b

Tactic:
coe_sup',

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑a ≤ s.sup (WithBot.some ∘ f) ↔ ∃ b ∈ s, a ≤ f b
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑a < ↑(s.sup' H f) ↔ ∃ b ∈ s, a < f b

Tactic:
coe_sup',

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑a < s.sup (WithBot.some ∘ f) ↔ ∃ b ∈ s, a < f b
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑(s.sup' H f) < ↑a ↔ ∀ i ∈ s, f i < a

Tactic:
coe_sup',

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup (WithBot.some ∘ f) < ↑a ↔ ∀ i ∈ s, f i < a
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Finite ι
f : ι → Set α
inst✝ : ∀ (i : ι), Finite ↑(f i)
this✝ : Fintype (PLift ι)
this : (i : ι) → Fintype ↑(f i)
⊢ Finite ↑(⋃ i, f i)

Tactic:
classical apply (fintypeiUnion _).finite

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst✝ : Finite ↑s
H : ∀ (t : ↑s), Finite ↑↑t
⊢ Finite ↑(⋃₀ s)

Tactic:
rw [sUnion_eq_iUnion]
  exact @Finite.Set.finite_iUnion _ _ _ _ H

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

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : IsEmpty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : Nonempty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i

Tactic:
· exact iInf_of_isEmpty (f i) ▸ inf_le_right

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : Nonempty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ sSup ∅ = ⊥

Tactic:
csSup_empty

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ ⊥ = ⊥
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Ico a b = {a} ↔ a ⋖ b

Tactic:
by
  simp [Ico_eq_singleton_iff]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ¬⨅ i, ↑(f i) = ⊤ ↔ Nonempty ι

Tactic:
iInf_coe_eq_top,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ¬IsEmpty ι ↔ Nonempty ι
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithTop α
⊢ a ⋖ ⊤ ↔ ∃ b, IsMax b ∧ a = ↑b

Tactic:
cases a with
  | coe a => simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]
  | top => simp [CovBy]

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

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

Tactic:
rw [sigmaLift, dif_pos rfl, mem_map]

Goal state after:
case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ ∃ a_1 ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) ⟨x.1, b⟩.snd, (Embedding.sigmaMk ⟨x.1, b⟩.fst) a_1 = x
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ ⟨i, x⟩ ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b

Tactic:
rw [sigmaLift, dif_pos rfl, mem_map]

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) ↔ x ∈ f a b