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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j ↦ q (i.succAbove j)) ≤ p

Tactic:
by
  simp [Pi.le_def, forall_iff_succAbove i]

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
⊢ Finite α

Tactic:
rcases exists_pair_ne α with ⟨x, y, hne⟩

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Finite α
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
this : x ∉ {i ∈ s | ¬p i}
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]

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

Goal state before:
pp: case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j

Tactic:
rwa [Fin.lt_def]

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

Goal state before:
pp: case cons
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a * s.prod)

Tactic:
by_cases hs_empty : s = ∅

Goal state after:
case pos
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)

case neg
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ p (a * s.prod)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
⊢ ((l ++ [a]).rotate' n).length = (a :: l).length

Tactic:
length_rotate' (l ++ [a]) n

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
⊢ (l ++ [a]).length = (a :: l).length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
← rotate_eq_drop_append_take (n.mod_lt hl).le,

Goal state after:
case inr
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = l.rotate (n % l.length)
Module: Mathlib.Data.List.Enum

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
p : α × ℕ → Prop
⊢ (∃ x, x ∈ l.zipIdx n ∧ p x) ↔ ∃ i x, p (l[i], n + i)

Tactic:
simp only [exists_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

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

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ choose 0 x✝ * x✝! * (0 - x✝)! = 0!

Tactic:
by simp [Nat.eq_zero_of_le_zero hk]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : LinearOrder α
⊢ #{x | x.1 < x.2} = (card α).choose 2

Tactic:
by
  simpa using Finset.card_product_filter_lt (s := univ)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

Tactic:
· rw [Pi.cons_ne _ h]

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

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
g h : G
⊢ (h * g⁻¹) • g • x₀ = h • x₀

Tactic:
simp [mul_smul]

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 α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
hy : y ∈ ⋂ i, f '' s i
⊢ y ∈ f '' ⋂ i, s i

Tactic:
simp only [mem_iInter, mem_image] at hy

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
hy : ∀ (i : ι), ∃ x ∈ s i, f x = y
⊢ y ∈ f '' ⋂ i, s i
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
m : M
p : Subsemigroup M
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
closure_le,

Goal state after:
M : Type u_1
inst✝ : Mul M
m : M
p : Subsemigroup M
⊢ {m} ⊆ ↑p ↔ m ∈ p
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: α : Type u_5
β : α → Type u_6
γ : (a : α) → β a → Type u_7
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : (a : α) → (b : β a) → One (γ a b)
a : α
b : β a
x : γ a b
⊢ uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x

Tactic:
rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t

Tactic:
by
  simp [not_disjoint_iff_nonempty_inter, mem_div, div_eq_one, Set.Nonempty]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
N N' : Submonoid M
⊢ N ⊔ N' = closure ↑N ⊔ closure ↑N'

Tactic:
closure_eq

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
m : M
p : Submonoid M
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
closure_le,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
m : M
p : Submonoid M
⊢ {m} ⊆ ↑p ↔ m ∈ p
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 β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s / t ⊆ range ⇑m

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩
  obtain ⟨a, rfl⟩ := hs ha
  obtain ⟨b, rfl⟩ := ht hb
  exact ⟨a / b, map_div ..⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S

Tactic:
by rw [mul_assoc, ← h, inv_mul_cancel_right]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H H' : Subgroup G
⊢ H ⊔ H' = closure ↑H ⊔ closure ↑H'

Tactic:
closure_eq

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
p : ι → Subgroup G
⊢ ⨆ i, p i = ⨆ i, closure ↑(p i)

Tactic:
closure_eq

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
by
  refine
    ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
  · intro y hy
    rw [eq_of_mem_singleton hy]
    exact ⟨1, zpow_one x⟩
  · exact ⟨0, zpow_zero x⟩
  · rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    exact ⟨n + m, zpow_add x n m⟩
  rintro _ _ ⟨n, rfl⟩
  exact ⟨-n, zpow_neg x n⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_7
inst✝ : Group N
f : G →* N
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
by rw [coe_range, coe_top]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M
⊢ x✝ ∈ mker 1 ↔ x✝ ∈ ⊤

Tactic:
simp [mem_mker]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : M
⊢ x ∈ mker (inl M N) ↔ x ∈ ⊥

Tactic:
simp [mem_mker]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : N
⊢ x ∈ mker (inr M N) ↔ x ∈ ⊥

Tactic:
simp [mem_mker]

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

Goal state before:
pp: m n : ℕ
⊢ pair m n < (max m n + 1) ^ 2

Tactic:
by
  simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]
  split_ifs <;> simp [Nat.le_of_lt, not_lt.1, *] <;> lia

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ closure {g} ≤ H ↔ g ∈ H

Tactic:
closure_le,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ {g} ⊆ ↑H ↔ g ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ closure s ≤ closure (⇑↑(MulAut.conj h) '' s)

Tactic:
closure_le,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ s ⊆ ↑(closure (⇑↑(MulAut.conj h) '' s))
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
⊢ a = 1

Tactic:
have ⟨q, eq⟩ := h.exists_left_inv
    rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ g, map (↑(MulAut.conj g)) H

Tactic:
by
  have : (⨅ g : G, H.map (MulAut.conj g) : Subgroup G).Normal := by
    refine normal_iff_map_conj_eq.mpr fun g ↦ ?_
    conv_rhs => rw [← Equiv.iInf_comp (Equiv.mulLeft g)]
    rw [map_iInf _ (MulAut.conj g).injective]
    simp [map_map, MulAut.mul_def]
  refine le_antisymm (le_iInf fun g ↦ ?_) ?_
  · grw [← Normal.map_conj_eq H.normalCore g, normalCore_le]
  · rw [normal_le_normalCore]
    apply iInf_le_of_le 1
    simp [MulAut.one_def]

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 α β
s : Set β
⊢ (∀ ⦃i j : α⦄, ¬Disjoint ((j⁻¹ * i) • s) s → i = j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
not_disjoint_iff_nonempty_inter

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
i : ι
⊢ h * g * h⁻¹ ∈ a i

Tactic:
exact (norm i).conj_mem g (g_in_iInf i) h

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

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Irrefl r
inst✝ : ∀ (i : ι), Std.Irrefl (s i)
i✝ : ι
a : α i✝
hi : r i✝ i✝
⊢ False

Tactic:
exact irrefl _ hi

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

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

pp: case inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ ⟨i, a⟩ = ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

Tactic:
· obtain hab | rfl | hba := trichotomous_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Or.inl rfl)
      · exact Or.inr (Or.inr <| Lex.right _ _ hba)

Goal state after:
case inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ ⟨i, a⟩ = ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (powerset ⟦l⟧).Nodup

Tactic:
simp only [quot_mk_to_coe, powerset_coe', coe_nodup]

Goal state after:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (List.map ofList l.sublists').Nodup
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ s.sup (f ⊔ g) = s.sup f ⊔ s.sup g

Tactic:
induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
  | cons _ _ _ ih =>
    rw [sup_cons, sup_cons, sup_cons, ih]
    exact sup_sup_sup_comm _ _ _ _

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)

Tactic:
refine hs.cons_induction ?_ ?_ <;> intros

Goal state after:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝ : ι
⊢ f ({a✝}.sup' ⋯ g) = {a✝}.sup' ⋯ (⇑f ∘ g)

case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : f (s✝.sup' hs✝ g) = s✝.sup' hs✝ (⇑f ∘ g)
⊢ f ((cons a✝¹ s✝ h✝).sup' ⋯ g) = (cons a✝¹ s✝ h✝).sup' ⋯ (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup' H f) = s.sup (g ∘ f)

Tactic:
← Finset.sup'_eq_sup H

Goal state after:
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)
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
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
have := hne.to_subtype
  rw [image_eq_range] at hf
  refine gc.l_ciSup_of_directed ?_ hf
  simpa [← directedOn_range, ← comp_def, range_comp]

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
this : ⋃ i, s i ⊆ ⋃ i ∈ t, s i
⊢ (⋃ i, s i).Finite

Tactic:
exact (ht.biUnion hs).subset this

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ i ∈ range f, t i

Tactic:
biUnion_range,

Goal state after:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ y, t (f y)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Sort v
κ : ι → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
intro ι

Goal state after:
α : Type u
ι✝ : Sort v
κ : ι✝ → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι✝
f : (a : ι✝) → κ a → α
ι : Type v
⊢ ∀ {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
rw [max_eq_left le]
    by_cases bdd : BddAbove (range f)
    · rw [← ciSup_subtype bdd le]
    · rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : (a ≤ b ∧ ∃ i, a i < b i) ∧ ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
⊢ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
⊢ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
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 γ
a : α x.1
b : β x.1
h : x.1 ≠ x.1
h✝ : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ False

Tactic:
exact h rfl

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ (Finset.Icc a a).val = {a}

Tactic:
Finset.Icc_self,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ {a}.val = {a}
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableLT α
inst✝ : DecidableLE α
a b x : α
⊢ x ∈ (Set.Ioo a b).toFinset ↔ a < x ∧ x < b

Tactic:
by simp only [Set.mem_toFinset, Set.mem_Ioo]

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
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }

Tactic:
have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by
      ext a b x
      rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]

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
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
hIoo : h₀_finset_Ioo = h₁_finset_Ioo
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hk : k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
⊢ k = l

Tactic:
rcases hk with ⟨hkn, rfl | hk⟩ <;> rcases hl with ⟨hln, rfl | hl⟩

Goal state after:
case succ.inl.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a

case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l