mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a

Tactic:
induction ac generalizing a with | intro _ H IH => ?_

Goal state after:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a

Tactic:
induction ac generalizing a with | intro _ H IH => ?_

Goal state after:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
c : Y
hc : f a < c ∧ c < f b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨EquivLike.inv f c, by simpa using hc⟩

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

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n

Tactic:
rw [p.pred_succ, q.pred_succ] at le

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
⊢ a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨c, rfl, rfl⟩; rw [← pow_mul, ← pow_mul']⟩
  by_cases m = 0; · simp_all
  by_cases n = 0; · simp_all
  by_cases hb : b = 0; · exact ⟨0, by simp_all⟩
  by_cases ha : a = 0; · exact ⟨0, by have := h.symm; simp_all⟩
  refine ⟨a ^ Nat.gcdB m n * b ^ Nat.gcdA m n, ?_, ?_⟩ <;>
  · refine (pow_one _).symm.trans ?_
    conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
    simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow,
      ← zpow_mul, mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]
    simp only [zpow_mul, zpow_natCast, h]
    exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
a : WithZero α
ha : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
by
    lift a to α using ha
    norm_cast
    apply mul_inv_cancel

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : b ≤ c
h2 : a ≤ c - b
⊢ c - b + b ≤ c

Tactic:
tsub_add_cancel_of_le h

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : b ≤ c
h2 : a ≤ c - b
⊢ c ≤ c
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
⊢ a ≤ b - c + c ↔ a ≤ b

Tactic:
tsub_add_cancel_of_le h

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b + b = a

Tactic:
tsub_add_cancel_of_le h

Goal state after:
case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a = a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (⇑f) 1 = 1

Tactic:
rw [WithTop.map_one, map_one, coe_one]

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

Goal state before:
pp: x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ exp (-↑(-y.log).toNat) ≤ y

Tactic:
rw [← WithZero.le_log_iff_exp_le hnz, Int.neg_le_iff]

Goal state after:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ -y.log ≤ ↑(-y.log).toNat
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ Nat.cast ⁻¹' Ioi a = Ioi ⌊a⌋₊

Tactic:
by
  ext
  simp [floor_lt, ha]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n + ↑n⌋₊ = ⌊a⌋₊

pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n

Tactic:
tsub_add_cancel_of_le h

Goal state after:
case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a⌋₊ = ⌊a⌋₊

R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
pow_add,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ k * a ^ k ↔ a ≠ 0
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
n : ℕ
n0 : 0 ≤ ↑n
⊢ |a ^ ↑n|ₘ = |a|ₘ ^ |↑n|

Tactic:
simp only [mabs_pow, zpow_natCast, Nat.abs_cast]

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ image2 f' (g' '' s) ((fun b ↦ b) '' t) = image2 f' (g' '' s) t

Tactic:
by rw [image_id']

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

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ image2 f' ((fun a ↦ a) '' s) (g' '' t) = image2 f' s (g' '' t)

Tactic:
by rw [image_id']

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

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ image2 f' (g' '' t) ((fun a ↦ a) '' s) = image2 f' (g' '' t) s

Tactic:
by rw [image_id']

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ image2 f' ((fun b ↦ b) '' t) (g' '' s) = image2 f' t (g' '' s)

Tactic:
by rw [image_id']

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}

Tactic:
← Ici_inter_Iic,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic b ∩ Icc b c = {b}
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulMono M
inst✝ : PosMulReflectLE M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ ≤ e₂) = (f₁ ≤ f₂)

Tactic:
subst H₁ H₂
  apply Iff.eq
  exact mul_le_mul_iff_right₀ HL

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

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)

Tactic:
simp only [beq_iff_eq]

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
l : List M
⊢ (filter (fun x ↦ x != 1) l).prod = l.prod

Tactic:
by
  classical induction l <;> grind

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ l[idxOf a l]? = some a

Tactic:
by
  rw [getElem?_eq_getElem (idxOf_lt_length_iff.2 h), getElem_idxOf]

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

Goal state before:
pp: case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ a * ((take n L).prod * (drop n L).prod * L[n]⁻¹) = L.prod * (L[n]⁻¹ * a)

Tactic:
prod_take_mul_prod_drop,

Goal state after:
case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ a * (L.prod * L[n]⁻¹) = L.prod * (L[n]⁻¹ * a)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑n * ↑a) (↑d * ↑a) = Rat.divInt ↑n ↑d

Tactic:
exact Rat.divInt_mul_right (mod_cast ha)

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

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

Tactic:
pow_add,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat c
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 ^ (b' + b') * -Int.ofNat a = -Int.ofNat c

Tactic:
pow_add,

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 ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat c
Module: Mathlib.Order.ConditionallyCompleteLattice.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
s : Set α
H : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
rw [BddAbove] at H

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
s : Set α
H : ¬(upperBounds s).Nonempty
⊢ sSup s = sSup ∅
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h

Tactic:
rw [← iSup_sup_eq]
  congr 1 with i
  split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j = ⨅ a, ⨆ b, ↑b

Tactic:
simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ (sSup (range f)).swap = sSup (range fun i ↦ (f i).swap)

Tactic:
swap_sSup,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ sSup (swap '' range f) = sSup (range fun i ↦ (f i).swap)
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, x ∈ Es i

Tactic:
simp [← mem_iUnion, Es_union]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
this : t = ∅
⊢ sSup ∅ = sSup t

Tactic:
rw [this]

Goal state after:
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
this : s = ∅
⊢ sSup s = sSup ∅

Tactic:
rw [this]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
⊢ Ioc a b = Ioc c d ↔ a = c ∧ b = d

Tactic:
by
  refine ⟨fun h ↦ ?_, by grind⟩
  have : b ≤ d ∧ c ≤ a := (Ioc_subset_Ioc_iff (show a < b by grind [Set.nonempty_Ioc])).1 h.subset
  have : d ≤ b ∧ a ≤ c := (Ioc_subset_Ioc_iff (show c < d by grind)).1 h.superset
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.1 = y.1
⊢ (fun p ↦ f p.1 p.2) y = f x.1 y.2

Tactic:
rw [this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.2 = y.2
⊢ (fun p ↦ f p.1 p.2) y = (fun a ↦ f a x.2) y.1

Tactic:
rw [this]

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
x : α
⊢ False

Tactic:
simp only [IsMaxChain, h', IsChain.empty, empty_subset, forall_const, true_and] at h

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h' : s = ∅
x : α
h : ∀ ⦃t : Set α⦄, IsChain r t → ∅ = t
⊢ False
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)

Tactic:
have : IsChain r s ∧ SuperChain r s h.choose := h.choose_spec

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s h.choose
⊢ SuperChain r s (SuccChain r s)
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
⊢ 0 ≤ ↑q

Tactic:
by
  rw [cast_def]; exact div_nonneg q.num.cast_nonneg q.den.cast_nonneg

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

Goal state before:
pp: m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m

Tactic:
by
  refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_gt h (factorial_le hmn), fun h => ?_⟩
  have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
    intro k hk
    rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
    exact Nat.mul_pos hk k.factorial_pos
  induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

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

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

Tactic:
rw [add_coe, sub_coe, if_pos h]
      exact add_tsub_cancel_of_le h.le

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ = z ↔ ↑z - ↑1 < a ∧ ⌈a⌉ ≤ z

Tactic:
← Int.cast_sub,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ = z ↔ ↑(z - 1) < a ∧ ⌈a⌉ ≤ z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ ⌈a⌉ = 0 ↔ a ∈ Ioc (-1) 0

Tactic:
by simp [ceil_eq_iff]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
n : ℤ
d : ℕ
res : ℤ
hres : round (↑n / ↑d) = res
⊢ IsRat r n d → IsInt (round r) res

Tactic:
by
  rintro ⟨inv, rfl⟩
  subst res
  constructor
  rw [invOf_eq_inv, ← div_eq_mul_inv]
  norm_cast

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

Goal state before:
pp: q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q

Tactic:
have : 0 + fract q < 1 := by simp [this]

Goal state after:
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : l₁ <+~ l₂
⊢ map f l₁ <+~ map f l₂

Tactic:
obtain ⟨l, hl_perm, hl_sub⟩ := a
    exact ⟨l.map f, hl_perm.map f, hl_sub.map f⟩

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b

Tactic:
exact cons_inj_left _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ (s - t).card + t.card = s.card

Tactic:
← card_add,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ (s - t + t).card = s.card
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)

Tactic:
by
  induction hst with
  | zero => simpa using huv
  | cons hab hst ih => simpa using ih.cons hab

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
h₂ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₂
⊢ False

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Goal state after:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ : α
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
n : a₁ ≠ a₁
h₂ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
mb₂ : b₁ ∈ l₂
⊢ False
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Goal state after:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ : α
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
n : a₁ ≠ a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
mb₂ : b₁ ∈ l₂ a₁
⊢ False
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
insert_of_not_mem h',

Goal state after:
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ (a :: l).Nodup
Module: Mathlib.Data.Multiset.Filter

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

Tactic:
by
  refine Multiset.induction_on s ?_ fun a t IH => ?_
  · rw [map_zero, countP_zero, filter_zero, card_zero]
  · rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
⊢ replicate n x ∩ s = replicate (min n (count x s)) x

Tactic:
by
  ext y
  rw [count_inter, count_replicate, count_replicate]
  by_cases h : x = y
  · simp only [h, if_true]
  · simp only [h, if_false, Nat.zero_min]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x M + count x N = count x P + count x Q

Tactic:
Multiset.ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), count a (M + N) = count a (P + Q)
x : α
⊢ count x M + count x N = count x P + count x Q
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
l : Multiset α
a : α
⊢ _root_.Disjoint l {a} ↔ ¬a ∈ l

Tactic:
rw [_root_.disjoint_comm, singleton_disjoint]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)

Tactic:
by_cases h : p a <;> simp [h]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
by simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x

Tactic:
by simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ ↔ ∀ (x : α), x ∈ s

Tactic:
by simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p s = univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s

Tactic:
by simp [Finset.ext_iff]

Goal state after: