mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

Tactic:
cases p.length_eq

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

Tactic:
cases p.length_eq

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval / l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h, zpow'_neg, div_eq_mul_inv, mul_inv, mul_assoc]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ l.eval ^ r = zpow' l.eval ↑r

Tactic:
rw [zpow'_ofNat _ hr]

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: ⊢ 1 /. 1 = 1

Tactic:
rw [divInt_one, Rat.intCast_one]

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ
⊢ q.toNNRat < p.toNNRat ↔ q < p ∧ 0 < p

Tactic:
by
  simp [← coe_lt_coe, toNNRat]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q * r) = ↑q * ↑r

Tactic:
by
  rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f r = g r

Tactic:
← r.num_div_den,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f (↑r.num / ↑r.den) = g (↑r.num / ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f r = g r

Tactic:
← r.num_div_den,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f (↑r.num / ↑r.den) = g (↑r.num / ↑r.den)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c

Tactic:
by
  subst_vars; rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ a * 0 < b * d

Tactic:
rw [mul_zero]
    exact mul_pos hab.pos hcd

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

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ f '' univ = range f

Tactic:
image_univ

Goal state after:
α : Type u_1
f : ℕ → α
⊢ range f = range f
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ x, f ↑x ⋯) ⊔ a = ⨆ x, f ↑x ⋯ ⊔ a

Tactic:
iSup_sup

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ ⨆ x, f ↑x ⋯ ⊔ a = ⨆ x, f ↑x ⋯ ⊔ a
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Tactic:
sUnion_eq_compl_sInter_compl,

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = (⋂₀ (compl '' compl '' S))ᶜ
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Ici (⨆ a ∈ s, a) = ⋂ a ∈ s, Ici a

Tactic:
Ici_iSup₂

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ ⋂ i ∈ s, Ici i = ⋂ a ∈ s, Ici a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
⊢ sSup s = sSup ∅

pp: case inr.inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
⊢ sSup s = sSup t

Tactic:
· have : s = ∅ := eq_empty_of_forall_notMem (fun x xs ↦ by simpa using hs x xs)
    rw [this]

Goal state after:
case inr.inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
⊢ sSup s = sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b

Tactic:
intro a ha
        exact coe_le_coe.1 (hb ha)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
⊢ Frame α

Tactic:
let completeLattice := e.completeLattice
  let heytingAlgebra := e.heytingAlgebra
  apply e.injective.frame <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case neg.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

pp: case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ b ∈ (fun a ↦ ↑a) ⁻¹' s, a ≤ b

Tactic:
· classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim

Goal state after:
case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ b ∈ (fun a ↦ ↑a) ⁻¹' s, a ≤ b
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ {a}.OrdConnected

Tactic:
rw [← Icc_self]
  exact ordConnected_Icc

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s

Tactic:
rw [disjoint_comm, mulSupport_disjoint_iff]

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

Goal state before:
pp: case inr
i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
· match i with
    | 0 => simp
    | 1 =>
      rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]
      exact Nat.mul_pos n.succ_pos n.succ.factorial_pos
    | succ (succ n) => contradiction

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

Goal state before:
pp: a b : ℕ+
h : b < a
⊢ a - b + b = a

Tactic:
rw [add_comm, add_sub_of_lt h]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ ≤ z - 1

Tactic:
le_sub_one_iff,

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ < z
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) ≤ (a + b) ^ 2 * (a + b) ^ (n + 1)

Tactic:
by
        gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a : R
Hsq : 0 ≤ a ^ 2
Hsq' : 0 ≤ (1 + a) ^ 2
H : 0 ≤ 2 + a
n : ℕ
⊢ 0 ≤ 2 * 1 + a

Tactic:
by simpa using H

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMagma G
inst✝¹ : Add H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f (a + x) = f x + b

Tactic:
rw [add_comm, map_add_const]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ max x 0 = y - (y - max x 0)

Tactic:
by rw [sub_sub_cancel]

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

Goal state before:
pp: case mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α)) l) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
exact Subperm.refl _

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ -(x -ᵥ y) = x -ᵥ y ↔ y = x

Tactic:
neg_eq_iff_add_eq_zero,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂
⊢ x₁ = x₂

Tactic:
neg_eq_iff_add_eq_zero,

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : x₁ -ᵥ x₂ + (x₁ -ᵥ x₂) = 0
⊢ x₁ = x₂
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ Surjective (map f)

Tactic:
intro s

Goal state after:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ a, map f a = s
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
⊢ s.strongInductionOn H = H s fun t _h ↦ t.strongInductionOn H

Tactic:
by
  rw [strongInductionOn]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α}, s ≤ 0 → s ≤ u → s ≤ 0 ∩ u

Tactic:
intro s

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s : Multiset α
⊢ ∀ {u : Multiset α}, s ≤ 0 → s ≤ u → s ≤ 0 ∩ u
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
⊢ ∀ {s u : Multiset α}, s ≤ a ::ₘ t → s ≤ u → s ≤ (a ::ₘ t) ∩ u

Tactic:
intro s

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s : Multiset α
⊢ ∀ {u : Multiset α}, s ≤ a ::ₘ t → s ≤ u → s ≤ (a ::ₘ t) ∩ u
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint s (t + u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
by
  rw [_root_.disjoint_comm, disjoint_add_left]; tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ.Nonempty ↔ Nonempty α

Tactic:
← coe_nonempty,

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ (↑univ).Nonempty ↔ Nonempty α
Module: Mathlib.Data.Fintype.OfMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
H : ∀ (x : α), x ∈ s
⊢ ∀ (x : α), x ∈ s.toFinset

Tactic:
by simpa using H

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l : List α
H : ∀ (x : α), x ∈ l
⊢ ∀ (x : α), x ∈ l.toFinset

Tactic:
by simpa using H

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f → a ∈ image (fun i ↦ f i) (range n)

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ a ∈ image (fun i ↦ f i) (range n)
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (i.rev.pred ⋯).rev

Tactic:
rev_pred,

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = i.rev.rev.castPred ⋯
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v - ↑n

Tactic:
rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> lia

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
⊢ b < a

Tactic:
simp [Fin.lt_def, -val_fin_lt] at *

Goal state after:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : ↑i < ↑a
hu : ↑b < ↑i + 1
⊢ ↑b < ↑a
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
⊢ a₁ ∈ ↑s → ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f' a₁ = f' x₂ → a₁ = x₂

Tactic:
ha₁

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f' a₁ = f' x₂ → a₁ = x₂
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n = n - (↑i % n + 1)

Tactic:
by
      rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]; exact i.modNat.rev.is_lt

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

Goal state before:
pp: case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ ¬x₀ ∈ Set.range x

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
i : Fin n
hi : x i = x₀
⊢ False
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
refine ⟨f, A, fun m n hmn => ?_⟩

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (f n)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (j.predAbove i).predAbove (i.succAbove j) = j

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, succAbove_of_castSucc_lt _ _ h, predAbove_of_le_castSucc,
      castPred_castSucc]
    rwa [le_castSucc_iff, succ_pred]

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α i.castSucc
i✝ : Fin n
y : α i✝.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ¬↑i < n
⊢ α (last n) = α i

Tactic:
by rw [eq_last_of_not_lt h]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ snoc (init q) (q (last n)) = q

Tactic:
by
  ext j
  cases j using Fin.lastCases <;> simp [init]

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

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ ¬x₀ ∈ Set.range x

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : x i = x₀
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
⊢ (∃ i, P i) → P (last n) ∨ ∃ i, P i.castSucc

Tactic:
rintro ⟨i, hi⟩

Goal state after:
n : ℕ
P : Fin (n + 1) → Prop
i : Fin (n + 1)
hi : P i
⊢ P (last n) ∨ ∃ i, P i.castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (∃ i, P i) → P p ∨ ∃ i, P (p.succAbove i)

Tactic:
rintro ⟨i, hi⟩

Goal state after:
n : ℕ
P : Fin (n + 1) → Prop
p i : Fin (n + 1)
hi : P i
⊢ P p ∨ ∃ i, P (p.succAbove i)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ StrictMono fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length

Tactic:
intro i j h
      dsimp only
      split_ifs with hi hj hj
      · rwa [Fin.val_fin_lt, f.lt_iff_lt]
      · lia
      · exact absurd (h.trans hj) hi
      · simpa using h

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

Goal state before:
pp: α : Type u_1
L : List (List α)
x : List α
⊢ x ++ (map (fun x_1 ↦ x_1 ++ x) L).flatten = (map (fun x_1 ↦ x ++ x_1) L).flatten ++ x

Tactic:
by
  induction L with grind

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

Goal state before:
pp: case insert
α : 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}))
⊢ fold op b (fun i ↦ if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]

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

Goal state before:
pp: α : 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
⊢ 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}))

Tactic:
by
  classical
    induction s using Finset.induction_on with
    | empty => simp [hb]
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]

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

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ (a' : List ℕ), a' ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint a'

Tactic:
intro s

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
⊢ s ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint s
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ ∀ (a_1 : List ℕ), a_1 ∈ l.ranges → (length ∘ map fun x ↦ a + x) a_1 = a_1.length

Tactic:
intro s

Goal state after:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
s : List ℕ
⊢ s ∈ l.ranges → (length ∘ map fun x ↦ a + x) s = s.length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ l.ranges.flatten

Tactic:
mem_flatten

Goal state after:
l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ ∃ l_1, l_1 ∈ l.ranges ∧ n ∈ l_1
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f : α → Multiset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (m.bind f) = m.bind fun a ↦ filter p (f a)

Tactic:
simp [bind, filter_join]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
x✝ : Option β
⊢ ((Option.map singleton x✝).getD 0).bind g = (Option.map g x✝).getD 0

Tactic:
cases f a with

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
⊢ iUnion (Fin.cons s f) = s ∪ ⋃ i, f i

Tactic:
ext
  simp [Fin.exists_iff_succ]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋃₀ S = ⋃ s ∈ S, a • s

Tactic:
by
  rw [sUnion_eq_biUnion, smul_set_iUnion₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ (f '' univ)ᶜ = (range f)ᶜ

Tactic:
image_univ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ (range f)ᶜ = (range f)ᶜ
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
by
  simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = (f '' s).seq t

Tactic:
rw [seq_eq_image2, image2_image_left]

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✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
w✝¹ : α
left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s
w✝ : α
left✝ : w✝ ∈ ⇑m ⁻¹' t
⊢ (fun x1 x2 ↦ x1 * x2) w✝¹ w✝ ∈ ⇑m ⁻¹' (s * t)

Tactic:
exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≠ ⊥ ↔ ∃ a, a ≠ 1

Tactic:
← nontrivial_iff_ne_bot,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ a, a ≠ 1