mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False

Tactic:
· have ab := xa.trans (h ⟨xa, xb⟩).2
      exact lt_irrefl _ (h ⟨ab, h'⟩).2

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

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)

Tactic:
rintro ⟨z, hz⟩ x hx y hy _

Goal state after:
case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
z : α
hz : ∀ (x : ι), x ∈ s → r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
a✝ : x ≠ y
⊢ (r on f) x y
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
⊢ x✝ ∈ f ⁻¹' c → ∀ ⦃y : α⦄, y ∈ f ⁻¹' c → x✝ ≠ y → (fun x y ↦ r x y ∨ r y x) x✝ y

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
⊢ ∀ ⦃y : α⦄, y ∈ f ⁻¹' c → x✝ ≠ y → (fun x y ↦ r x y ∨ r y x) x✝ y
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a % b = ↑r

Tactic:
obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
  simp only [← h, ← hm, Int.add_mul_emod_self_right]
  rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]

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

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ extend f g 1 x = 1

Tactic:
extend_apply' _ _ _ hf

Goal state after:
case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ 1 x = 1
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
⊢ extend f g 1 x = 1

Tactic:
by_cases hf : ∃ a, f a = x
    · rw [extend, dif_pos hf, ← notMem_mulSupport]
      rw [← Classical.choose_spec hf] at hfg
      exact fun hg ↦ hfg ⟨_, hg, rfl⟩
    · rw [extend_apply' _ _ _ hf]; rfl

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → (n + 1) ^ 0 < (n + 1).ascFactorial 0

Tactic:
by rintro ⟨⟩

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial (k + 1) ≤ (n + (k + 1)) ^ (k + 1)

Tactic:
by
    rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]
    exact Nat.mul_le_mul_right _
      (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → (n + 1).ascFactorial 0 < (n + 0) ^ 0

Tactic:
by rintro ⟨⟩

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

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt (le_refl _) (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _)
      (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → 0 ≤ n → (n + 1 - 0) ^ 0 < n.descFactorial 0

Tactic:
by rintro ⟨⟩

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 ≤ 0 → n.descFactorial 0 < n ^ 0

Tactic:
by rintro ⟨⟩

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

Goal state before:
pp: case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → m.mod k = k

pp: case mpr
k m : ℕ+
⊢ m.mod k = k → ↑m % ↑k = 0

Tactic:
· intro h
    apply PNat.eq
    rw [mod_coe, if_pos h]

Goal state after:
case mpr
k m : ℕ+
⊢ m.mod k = k → ↑m % ↑k = 0
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ (fun x ↦ x ^ n) a ≤ (fun x ↦ x ^ n) b

Tactic:
rw [← one_le_div', ← div_zpow]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
n : ℕ
⊢ ⌊a / ↑n⌋ = ⌊a⌋ / ↑n

Tactic:
by
  simpa using floor_div_cast_of_nonneg n.cast_nonneg a

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

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = c * q.num / ↑d

Tactic:
d_eq_c_mul_denom

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = c * q.num / (c * ↑q.den)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : a ^ (m + 1) ≤ g
⊢ ∃ z ∈ s, m < z

Tactic:
exact ⟨m + 1, hm', lt_add_one _⟩

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs

Tactic:
have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
⊢ q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉ / b⌉ ≤ b * (↑⌈(b - 1)⁻¹⌉ / b)

pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
⊢ ↑⌈a⌉ ≤ b * a

Tactic:
· rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]
    positivity

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
⊢ ↑⌈a⌉ ≤ b * a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inr.refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : a < (c ^ n)⁻¹
⊢ a < c ^ (-↑n)

Tactic:
← zpow_natCast,

Goal state after:
case inr.inr.inr.refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : a < (c ^ ↑n)⁻¹
⊢ a < c ^ (-↑n)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inr.refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : (c ^ n)⁻¹ < b
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b

Tactic:
← zpow_natCast,

Goal state after:
case inr.inr.inr.refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : (c ^ ↑n)⁻¹ < b
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p₁ /ₛ p = p₂ /ₛ p
⊢ p₁ = p₂

Tactic:
rwa [← div_eq_one, sdiv_div_sdiv_cancel_right, sdiv_eq_one_iff_eq] at h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ s.attach
⊢ (a = x✝¹) = (↑a = ↑x✝¹)

Tactic:
by simp [Subtype.ext_iff]

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

Goal state before:
pp: case mk
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk (⇑(isSetoid α)) l)

Tactic:
induction l with | nil => exact empty | cons _ _ ih => exact cons _ _ ih

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

Goal state before:
pp: α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
⊢ l[i] = l[j] ↔ i = j

Tactic:
have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩
  simpa

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
by
  constructor
  · generalize hm : a ::ₘ as = m
    intro h
    induction h generalizing as with
    | zero => simp at hm
    | @cons a' b as' bs ha'b h ih =>
      rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
      · exact ⟨b, bs, ha'b, h, rfl⟩
      · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
  · exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
⊢ a ∈ x ::ₘ s → ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
ha

Goal state after:
case cons
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha : a ∈ x ::ₘ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs ⊆ ys → xs ∪ ys = ys
h : x :: xs ⊆ ys
⊢ List.insert x (xs ∪ ys) = ys

Tactic:
insert_of_mem <| mem_union_right _ <| h mem_cons_self,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs ⊆ ys → xs ∪ ys = ys
h : x :: xs ⊆ ys
⊢ xs ∪ ys = ys
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ (s + t).dedup = s.dedup + t.dedup

Tactic:
induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.dedup_append (by simpa using h)

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s

Tactic:
rw [filter_cons_of_pos _ h, singleton_add]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
⊢ count (f x) (map f s) = count x s

Tactic:
by_cases H : x ∈ s

Goal state after:
case pos
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s

Tactic:
mem_image,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ a ∈ s, f a = a✝) ↔ ∃ a ∈ s, g a = a✝
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⟩
    simp only [mem_image, mem_range]
    exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i < n, f ↑i = a
i : ℕ
hi : i < n
ha : f ↑i = a
⊢ f (↑i % ↑n) = a

Tactic:
Int.emod_eq_of_lt (Int.natCast_nonneg _) (Int.ofNat_lt_ofNat_of_lt hi),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i < n, f ↑i = a
i : ℕ
hi : i < n
ha : f ↑i = a
⊢ f ↑i = a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i < n, f ↑i = a
i : ℕ
hi : i < n
ha : f ↑i = a
⊢ f ↑i = a

Tactic:
ha

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i < n, f ↑i = a
i : ℕ
hi : i < n
ha : f ↑i = a
⊢ a = a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset ↑t
a : α
⊢ a ∈ ↑(map (Embedding.subtype fun x ↦ x ∈ t) s) → a ∈ t

Tactic:
ha

Goal state after:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ ↑(map (Embedding.subtype fun x ↦ x ∈ t) s)
⊢ a ∈ t
Module: Mathlib.Data.Fin.Basic

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

Tactic:
rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n = ↑↑u - ↑↑v

case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u) - ↑n

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n < ↑n
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]

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n = ↑↑u + ↑↑v - ↑n

case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v) - ↑n

case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

Tactic:
by
  rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2),
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]

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

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

pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
· rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ ((a.castPred ha).succAbove (b.castPred hb)).castSucc = ((a.succAbove b).castPred hk).castSucc

Tactic:
← castSucc_succAbove_castSucc,

Goal state after:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ (a.castPred ha).castSucc.succAbove (b.castPred hb).castSucc = ((a.succAbove b).castPred hk).castSucc
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)

Tactic:
← ofFn_id,

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (ofFn id)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_1.inr
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}

Tactic:
exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩

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

Goal state before:
pp: case h
α : 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'
n : ℕ
IH : ∀ m < n, P (f m)
⊢ P (f n)

Tactic:
| _ n IH
       => 

Goal state after:
case h
α : 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'
n : ℕ
IH : ∀ m < n, P (f m)
⊢ P (f n)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + n = m

Tactic:
hv,

Goal state after:
m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + 0 = m
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ card { _a // True } = card α

Tactic:
apply Fintype.card_of_subtype

Goal state after:
α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ ∀ (x : α), x ∈ univ ↔ True
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case refine_2.inr
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l

Tactic:
· exact h.cons_duplicate

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
⊢ α (i.castLT h).castSucc = α i

Tactic:
by rw [Fin.castSucc_castLT i h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x

Tactic:
exact
    ⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩,
     fun ⟨x, hx⟩ =>
      ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ =>
          Subsingleton.elim _ _⟩⟩⟩

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
⊢ ⋯ ▸ p ((i.succAbove j).castPred ⋯) = p j

Tactic:
generalize_proofs H₁ H₂

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).castPred H₁) = p j
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ l

Tactic:
apply hab.subset

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ [a, b]
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

Tactic:
apply hab.subset

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Tactic:
apply hab.subset

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case pos
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : l = []
⊢ l'.head! ≤ l.head!

Tactic:
simp [hl] at h

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
by
  induction l using twoStepInduction with grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
σ : α → Type u_8
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (l₁.sigma l₂).length = (map (fun a ↦ (l₂ a).length) l₁).sum

Tactic:
induction l₁ with
  | nil => rfl
  | cons x l₁ IH => simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
⊢ ∀ (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)

Tactic:
ha

Goal state after:
case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
⊢ filter p (n • ha) = n • filter p ha → filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ countP p (n • s) = n * countP p s

Tactic:
by
  induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
s : Multiset α
⊢ count a (n • s) = n * count a s

Tactic:
by
  induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

Goal state after: