mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
generalize hc : c /. d = x

Goal state after:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
x : ℚ
hc : c /. d = x
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } x = f₁ a b c d /. f₂ a b c d
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * z) y ↔ IsRelPrime y z

Tactic:
isRelPrime_mul_unit_left_left hu,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime z y ↔ IsRelPrime y z
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z

Tactic:
by
  rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

Tactic:
isRelPrime_mul_unit_left_left hu,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : GroupWithZero α
m n : α
x✝ : m ∣ n
hm : m = 0
a : α
ha : n = m * a
⊢ n = 0

pp: case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n

Tactic:
· simp [hm, ha]

Goal state after:
case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n d : ℤ
d_ne_zero : d ≠ 0
⊢ ↑n / ↑d = n /. d

Tactic:
rw [← Rat.divInt_eq_div]

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

Goal state before:
pp: case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c

pp: case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d

Tactic:
· rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]

Goal state after:
case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (-Int.ofNat a) ^ (2 * b' + 1) = -Int.ofNat c

Tactic:
pow_succ,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (-Int.ofNat a) ^ (2 * b') * -Int.ofNat a = -Int.ofNat c
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: α : Type u
x : BinaryTree α
⊢ 0 < x.numLeaves

Tactic:
by
  rw [numLeaves_eq_numNodes_succ]
  exact x.numNodes.zero_lt_succ

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a b : R
x✝ : -1 * a = b
⊢ -a = b

Tactic:
by subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ : R
a₂ : ℕ
a₃ b : R
x✝ : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Tactic:
by subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a₁ : R
a₂ : ℕ
a₃ b₁ b₃ c : R
x✝² : a₁⁻¹ = b₁
x✝¹ : a₃⁻¹ = b₃
x✝ : b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c
⊢ (a₁ ^ a₂ * a₃)⁻¹ = c

Tactic:
by subst_vars; simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i

Tactic:
rw [← Monotone.iSup_nat_add hf k]

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ

Tactic:
rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
s : Set β
t : Set γ
f : β → γ
g : γ → α
hf : BijOn f s t
⊢ ⨆ x ∈ s, g (f x) = ⨆ y ∈ t, g y

Tactic:
← hf.image_eq,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
s : Set β
t : Set γ
f : β → γ
g : γ → α
hf : BijOn f s t
⊢ ⨆ x ∈ s, g (f x) = ⨆ y ∈ f '' s, g y
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
simp_rw [union_distrib_iInter_left]

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J
⊢ x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ i ∈ Iᶜ

Tactic:
obs',

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J
⊢ i ∉ I ↔ i ∈ Iᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f : ι → α
⊢ (iSup f)ᶜᶜ = (⨅ i, (f i)ᶜ)ᶜ

Tactic:
by simp [compl_iInf]

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

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsLUB s (sSup s)

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · simp [sSup]
  · exact isLUB_sSup' hs

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s

Tactic:
rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']

Goal state after:
case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
by
  have : Std.Symm fun a b ↦ a ≺ b ∨ b ≺ a := { symm _ _ := Or.symm }
  rw [IsChain, IsChain, IsChain, pairwise_union_of_symm]

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹

Tactic:
by
  rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]

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

Goal state before:
pp: n : ℕ
⊢ n ! * 1 = n !

Tactic:
Nat.mul_one

Goal state after:
n : ℕ
⊢ n ! = n !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n + 1 = (n + 1) * 1

Tactic:
Nat.mul_one

Goal state after:
n : ℕ
⊢ n + 1 = n + 1
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : CommMagma β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b : α
⊢ f a ≤ f b * f (a / b)

Tactic:
by
  simpa only [mul_comm, div_mul_cancel] using map_mul_le_mul f (a / b) b

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

Goal state before:
pp: n k : ℕ
h : k.succ ≤ n.succ
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !

Tactic:
rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]

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

Goal state before:
pp: m n : ℕ+
⊢ m ∣ n → m ≤ n

Tactic:
by
  rw [dvd_iff']
  intro h
  rw [← h]
  apply (mod_le n m).left

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
⊢ ¬IsCyclic α

Tactic:
by
  intro h
  rcases exists_zpow_surjective α with ⟨a, ha⟩
  rcases lt_trichotomy a 1 with hlt | rfl | hlt
  · rcases exists_between hlt with ⟨b, hab, hb⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by lia
    rw [← one_lt_inv'] at hlt
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all
  · rcases exists_ne (1 : α) with ⟨b, hb⟩
    simpa [hb.symm] using ha b
  · rcases exists_between hlt with ⟨b, hb, hba⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by lia
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all

Goal state after:
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
b a : k
hb : 0 < b
⊢ a < b + ↑⌊a / b⌋ * b

Tactic:
by
    rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]
    exact lt_floor_add_one _

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

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst✝³ : CommGroup G
inst✝² : PartialOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
x y : Gᵒᵈ
hy✝ : 1 < y
hy : ofDual y < 1
n : ℕ
hn : (ofDual x)⁻¹ ≤ (ofDual y)⁻¹ ^ n
⊢ x ≤ y ^ n

Tactic:
by rwa [inv_pow, inv_le_inv_iff] at hn

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
⊢ (fract q⁻¹).num < q.num

Tactic:
suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]

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 - ↑⌊q_inv⌋).num < q.num
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: 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
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred.succ < b * c
hn : Nat.find this ≠ 0
⊢ False

Tactic:
pow_succ,

Goal state after:
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
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred * c < b * c
hn : Nat.find this ≠ 0
⊢ False
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
s : Multiset α
inst✝ : DecidableEq α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α)) _l) ↔
    ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → count a (Quot.mk (⇑(isSetoid α)) _l) = 1

Tactic:
by simpa using List.nodup_iff_count_eq_one

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b

Tactic:
by
  induction h with
  | zero => simp
  | @cons x y s t hxy _ ih =>
    intro a ha
    rcases mem_cons.1 ha with ha | ha
    · exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
    · rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
f : α → β
x : α
y : β
⊢ map (update f x y) l = if x ∈ l then (map f l).set (idxOf x l) y else map f l

Tactic:
induction l with | nil => simp | cons hd tl ihl => ?_
  rw [nodup_cons] at hl
  simp only [mem_cons, map, ihl hl.2]
  by_cases H : hd = x
  · subst hd
    simp [hl.1]
  · simp [Ne.symm H, H, ← apply_ite (cons (f hd))]

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

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹

Tactic:
simp_rw [@ne_comm _ b]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ (↑s.toFinset).Nonempty ↔ s.Nonempty

Tactic:
coe_toFinset

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.Nonempty ↔ s.Nonempty
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ ↑s.toFinset ⊂ ↑t ↔ s ⊂ ↑t

Tactic:
coe_toFinset

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s ⊂ ↑t ↔ s ⊂ ↑t
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ ↑s ⊆ ↑t.toFinset ↔ ↑s ⊆ t

Tactic:
coe_toFinset

Goal state after:
α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ ↑s ⊆ t ↔ ↑s ⊆ t
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ ↑s ⊂ ↑t.toFinset ↔ ↑s ⊂ t

Tactic:
coe_toFinset

Goal state after:
α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ ↑s ⊂ t ↔ ↑s ⊂ t
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ ↑s.toFinset ⊆ ↑t ↔ s ⊆ ↑t

Tactic:
coe_toFinset

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s ⊆ ↑t ↔ s ⊆ ↑t
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ (↑s.toFinset).Nontrivial ↔ s.Nontrivial

Tactic:
coe_toFinset

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.Nontrivial ↔ s.Nontrivial
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
⊢ (s ∆ t).toFinset = s.toFinset ∆ t.toFinset

Tactic:
ext
  simp [mem_symmDiff, Finset.mem_symmDiff]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t

Tactic:
refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ image f (map (Embedding.subtype fun x ↦ x ∈ s) t) = image (f ∘ Subtype.val) t
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' : α → β := ⋯
⊢ Set.InjOn f' ↑s

Tactic:
intro a₁

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₁ : α
⊢ a₁ ∈ ↑s → ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f' a₁ = f' x₂ → a₁ = x₂
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * ↑i + m * 1

Tactic:
Nat.mul_one

Goal state after:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * ↑i + m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j

Tactic:
let finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m)
    invFun i := @Fin.addCases m n (fun _ => Fin m ⊕ Fin n) Sum.inl Sum.inr i
    left_inv x := by rcases x with y | y <;> simp
    right_inv x := by refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp }
  rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp,
    Equiv.coe_fn_mk]

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

Goal state before:
pp: n m : ℕ
h : Fin n = Fin m
⊢ cast h = Fin.cast ⋯

Tactic:
cases fin_injective h
  rfl

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

Goal state before:
pp: m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
⊢ append as (snoc bs b) = snoc (append as bs) b

Tactic:
by
  funext i
  rcases i with ⟨i, isLt⟩
  simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1,
    eq_rec_constant, Nat.add_eq]
  split_ifs with lt_n lt_add sub_lt nlt_add lt_add <;> (try rfl)
  · have := Nat.lt_add_right m lt_n
    contradiction
  · obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt
    simp [Nat.add_comm n m] at sub_lt
  · have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add
    contradiction

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc x x₀)
x : (i : Fin n) → init α i
x₀ : α (last n)
⊢ snoc x (Fin.snoc x x₀ (last n)) ≍ snoc x x₀

Tactic:
Fin.snoc_last

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc x x₀)
x : (i : Fin n) → init α i
x₀ : α (last n)
⊢ snoc x x₀ ≍ snoc x x₀
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ #s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
rw [← Fintype.card_coe] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
g : (j : Fin (n + 1)) → α j
⊢ g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f

Tactic:
simpa [eq_comm] using insertNth_eq_iff

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
⊢ h.toFinset = hs.toFinset ∆ ht.toFinset

Tactic:
ext
  simp [mem_symmDiff, Finset.mem_symmDiff]

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

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

Tactic:
exact Fin.le_iff_val_le_val.2 (le_of_lt h)

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

Goal state before:
pp: case cons.tail
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
a✝ : Mem a tail✝
⊢ R (head✝ :: tail✝).head! a

Tactic:
| tail =>

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

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

Tactic:
← isChain_iff_pairwise,

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h :: t).prod

Tactic:
simp only [List.prod_cons]
    exact IsUnit.mul (u h mem_cons_self) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ (a :: l₁ ++ l₂).alternatingProd = (a :: l₁).alternatingProd * l₂.alternatingProd ^ (-1) ^ (a :: l₁).length

Tactic:
simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List.chains r
acc : ∀ (a : α), a ∈ (↑l).head? → Acc r a
⊢ Acc (List.lex_chains r) l

Tactic:
obtain ⟨_ | ⟨a, l⟩, hl⟩ := l

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ Acc (List.lex_chains r) ⟨[], hl⟩

case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
⊢ ∀ (a : α), a ∈ m → (if p a then {a} else 0).bind f = if p a then f a else 0

Tactic:
intro a ham

Goal state after:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
⊢ (if p a then {a} else 0).bind f = if p a then f a else 0
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f : α → Option β
⊢ filterMap f m = m.bind fun a ↦ (Option.map singleton (f a)).getD 0

Tactic:
induction m using Multiset.induction with
  | empty => simp
  | cons a m ih => simp [filterMap_cons, ih]

Goal state after: