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

Goal state before:
pp: n : ℤ
⊢ n /. 1 = ↑n

Tactic:
by simp [divInt, mkRat, normalize]

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

Goal state before:
pp: ⊢ 1 /. 1 ≠ 0

Tactic:
divInt_ne_zero

Goal state after:
⊢ 1 ≠ 0

⊢ 1 ≠ 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a b c : ℤ
h : c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
h : q ≠ 0
⊢ ↑(q * q⁻¹) = ↑1

Tactic:
simp [h]

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a

Tactic:
refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
    c.dvd_of_dvd_mul_right ?_

Goal state after:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ n.natAbs ∣ a.natAbs * d
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑(q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs

Tactic:
Int.dvd_natAbs

Goal state after:
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den + q₂.num * ↑q₁.den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p - q) = ↑p - ↑q

Tactic:
by simp [sub_eq_add_neg, cast_add_of_ne_zero, hp, hq]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
x✝ : R a 0
h : b = 0
⊢ a * b = 0

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
h : a = 0
x✝ : R b 0
⊢ a * b = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (ad * bd * a < ad * bd * b)

pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
mul_lt_mul_iff_right₀

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (a < b)

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ max a b = b

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x

Tactic:
by
      { rw [iSup_union, iSup_singleton, iSup_range] }

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : ¬p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ i ∈ s, i

Tactic:
← sInter_image,

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂₀ ((fun i ↦ i) '' s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
⊢ IsLUB ∅ (sSup ∅)

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rcases exists_between h₁ with ⟨x, xa, xb⟩

Goal state after:
α : 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₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
s : Set (WithTop α)
h : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
s : Set (WithBot α)
h : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
simp [h]

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

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ (if ⊤ ∈ S then ⊤ else if BddAbove ((fun a ↦ ↑a) ⁻¹' S) then ↑(sSup ((fun a ↦ ↑a) ⁻¹' S)) else ⊤) ≤ a

Tactic:
simp [h]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : b ≤ a
⊢ b = c

Tactic:
have hb := (h b).not

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : b ≤ a
hb : b ∉ (fun b ↦ Ι b a) b ↔ b ∉ (fun b ↦ Ι b a) c
⊢ b = c
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ ↑S ⊆ ↑T ∧ ↑S ≠ ↑T ↔ S < T

Tactic:
lt_iff_le_and_ne,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ ↑S ⊆ ↑T ∧ ↑S ≠ ↑T ↔ S ≤ T ∧ S ≠ T
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
⊢ IsStrongAntichain r' (f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
⊢ ¬r' (f a) c ∨ ¬r' (f b) c
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = sSup ∅

Tactic:
simp [ht]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : ¬BddBelow t
⊢ sInf t = sInf ∅

Tactic:
simp [ht]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ sInf (Subtype.val '' S) ∈ Icc a b

Tactic:
by
    rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS
    refine ⟨le_csInf (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.1), ?_⟩
    obtain ⟨c, hc⟩ := hS
    exact le_trans (csInf_le ⟨a, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.1⟩ ⟨c, hc, rfl⟩) c.2.2

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : a = 1
⊢ mulSupport (mulSingle i a) = ∅

Tactic:
simp [h]

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : ¬a = 1
⊢ mulSupport (mulSingle i a) = {i}

Tactic:
simp [h]

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 = a⁻ᵐ⁻¹

Tactic:
oneLePart_div_leOnePart,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊓ 1 = a⁻ᵐ⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case step
i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + m✝.succ ! < (i + m✝.succ)!

Tactic:
exact add_factorial_succ_lt_factorial_add_succ _ hi

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)

Tactic:
succ_descFactorial _ k,

Goal state after:
n k : ℕ
⊢ (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial (k + 1)
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 2 * fract x ∈ Ico 0 1

Tactic:
simp [h]

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

Goal state before:
pp: case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ ↑k * n.succ = ↑(k * ⟨n.succ, ⋯⟩)

Tactic:
mul_coe,

Goal state after:
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ ↑k * n.succ = ↑k * ↑⟨n.succ, ⋯⟩
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a✝ : R
z a : ℤ
⊢ ↑a ≤ a✝ + ↑z ↔ a ≤ ⌊a✝⌋ + z

Tactic:
← sub_le_iff_le_add,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a✝ : R
z a : ℤ
⊢ ↑a - ↑z ≤ a✝ ↔ 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
inst✝ : IsOrderedRing R
a✝ : R
z a : ℤ
⊢ ↑a - ↑z ≤ a✝ ↔ a ≤ ⌊a✝⌋ + z

Tactic:
← sub_le_iff_le_add,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a✝ : R
z a : ℤ
⊢ ↑a - ↑z ≤ a✝ ↔ a - z ≤ ⌊a✝⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Tactic:
← sub_le_iff_le_add,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a + b⌋ - 1 - ⌊b⌋ ≤ ⌊a⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + b - (↑⌊a⌋ + ↑⌊b⌋) ≤ a + b - (↑⌊a + b⌋ - 1)

Tactic:
sub_le_sub_iff_left

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ fract 1 = 0

Tactic:
simp [fract]

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
inst✝ : IsOrderedRing R
n : ℕ
⊢ fract ↑n = 0

Tactic:
simp [fract]

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

Goal state before:
pp: case inr.inr.inl
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₁ : a < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

pp: case inr.inr.inr
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
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
· refine ⟨0, ?_⟩
        rw [zpow_zero]
        exact ⟨ha₁, hb₁⟩

Goal state after:
case inr.inr.inr
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
⊢ ∃ n, a < c ^ n ∧ c ^ n < b
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ b⁻¹ * a < c

Tactic:
inv_mul_lt_iff₀ hb₀

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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ a < b * c
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a : α
⊢ a ∈ {a}

Tactic:
rw [← cons_zero]
  exact mem_cons_self _ _

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

Goal state before:
pp: case mp
α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) s t → s = t

Tactic:
intro h
    induction h <;> simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b' ∈ f a

Tactic:
rw [← e]; exact bm

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s

Tactic:
obtain ⟨y, rfl⟩ := hf x
    obtain ⟨t, rfl⟩ := ih
    exact ⟨y ::ₘ t, map_cons _ _ _⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
  · simpa only [dedup, forall_mem_ne, not_not] using this
  · intro x y z xz
    exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (ndinsert a s).card = s.card

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (ndinsert a s).card = s.card + 1

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
xs : List α
x : α
⊢ xs <:+: [x] ↔ xs = [] ∨ xs = [x]

Tactic:
match xs with
  | [] => simp
  | [_] => simp [List.singleton_infix_singleton_iff]
  | _ :: _ :: _ =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · simp

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

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
⊢ s.disjUnion {a} h = cons a s ⋯

Tactic:
by
  rw [disjUnion_comm, singleton_disjUnion]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∈ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∉ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ a ∉ s \ t

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} ∩ s = {a}

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ {a} ∩ s = ∅

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

Tactic:
refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · grind
    · grind
    · intro x
      simp only [coe_filter, Set.mem_ofPred_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
a : α
s : Finset α
ha : a ∉ s
⊢ f a ∉ map f s

Tactic:
by simpa using ha

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ s.toFinset = t.toFinset

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (image Subtype.val s.attach).val = s.val

Tactic:
by rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c

Tactic:
· rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]
    exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ #({x ∈ s | f x = y}) ≠ 0 ↔ y ∈ image f s

Tactic:
← Nat.pos_iff_ne_zero,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ 0 < #({x ∈ s | f x = y}) ↔ y ∈ image f s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
by
  let f' : s → β := fun a ↦ f a a.2
  have hinj' : Set.InjOn f' s.attach := fun x hx y hy hxy ↦ Subtype.ext (hinj _ _ x.2 y.2 hxy)
  have hmapsto' : Set.MapsTo f' s.attach t := fun x hx ↦ hf _ _
  intro b hb
  obtain ⟨a, ha, rfl⟩ := surjOn_of_injOn_of_card_le _ hmapsto' hinj' (by rwa [card_attach]) hb
  exact ⟨a, a.2, rfl⟩

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 1)
⊢ (∃ z, x.succAbove z = y) → y ≠ x

Tactic:
rintro ⟨y, rfl⟩

Goal state after:
n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (ofFn f).Nodup

Tactic:
by
  rw [ofFn_eq_pmap]
  exact nodup_range.pmap fun _ _ _ _ H => Fin.val_eq_of_eq <| hf H

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j

Tactic:
cases j using Fin.cases <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst✝ : Decidable p
x✝ : PLift p
h : p
⊢ { down := h } ∈ if h : p then {{ down := h }} else ∅

Tactic:
simp [h]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
j : Fin (n + 1)
h : j ≠ 0
⊢ (predAbove 0 j).succ = j

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ (fun a ↦ ⟨f a, ⋯⟩) a = ⟨val✝, ⋯⟩

Tactic:
by simpa using ha

Goal state after: