mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b ^ (↑m * m.gcdA n + ↑n * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
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)]

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b ^ (↑m * m.gcdA n) * b ^ (↑n * m.gcdB n) = a ^ (↑m * m.gcdB n) * b ^ (↑m * m.gcdA n)
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulZeroOneClass β
f : α →* β
hf : Surjective ⇑f
⊢ Surjective ⇑(lift' f)

Tactic:
intro b
  obtain ⟨a, rfl⟩ := hf b
  exact ⟨a, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z) → (fun x1 x2 ↦ x1 < x2) y z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝² + a✝¹ < a✝² + a✝ → a✝¹ < a✝
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 : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b + c = a + c - b

Tactic:
by rw [add_comm a, hb.add_tsub_assoc_of_le h, add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ 0 < a - b ↔ b < a

Tactic:
tsub_pos_iff_not_le,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ ¬a ≤ b ↔ b < a
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : |x| ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0

pp: case inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Tactic:
· simp [le_total 0 x]

Goal state after:
case inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z) → (fun x1 x2 ↦ x1 < x2) y z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝² + a✝¹ < a✝² + a✝ → a✝¹ < a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ ⊥ + ↑a✝ ≤ ↑(a✝¹ + a✝) ↔ ⊥ ≤ ↑a✝¹

Tactic:
aesop (add simp WithTop.add_le_add_iff_right)

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ ↑(a✝¹ + a✝) ≤ ⊥ + ↑a✝ ↔ ↑a✝¹ ≤ ⊥

Tactic:
aesop (add simp WithTop.add_le_add_iff_right)

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝² a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ a✝² + a✝ ≤ a✝¹ + a✝ ↔ a✝² ≤ a✝¹

Tactic:
aesop (add simp WithTop.add_le_add_iff_right)

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

Goal state before:
pp: case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]
      refine iff_of_true ?_ le_self_add
      exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg

Goal state after:
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
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌊a + 1⌋₊ = ⌊a⌋₊ + 1

Tactic:
← cast_one,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌊a + ↑1⌋₊ = ⌊a⌋₊ + 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
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 : ℕ
han : a ≤ ↑n
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) ≤
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))

Tactic:
gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (b - a) / b = 1 - a / b

Tactic:
by
  simpa only [← @div_self _ _ b h] using (div_sub_div_same b a b).symm

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ c ^ n = c ^ n + (b ^ n + d ^ n)

Tactic:
hn.pow_add_pow_eq_zero hbd.symm,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ c ^ n = c ^ n + 0
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝¹ b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ : (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2)ᵒᵈ
a : α
⊢ Quotient.mk'' (id (id a)) = Quotient.mk'' a

Tactic:
id

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝¹ b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ : Antisymmetrization αᵒᵈ fun x1 x2 ↦ x1 ≤ x2
a : αᵒᵈ
⊢ Quotient.mk'' (id (id a)) = Quotient.mk'' a

Tactic:
id

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ ⇑(ofInjective f hf).symm = rangeSplitting f

Tactic:
ext ⟨y, x, rfl⟩

Goal state after:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
x : α
⊢ (ofInjective f hf).symm ⟨f x, ⋯⟩ = rangeSplitting f ⟨f x, ⋯⟩
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Ioc a b \ {b} = Ioo a b

Tactic:
Ioc_sdiff_right

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Ioo a b = Ioo a b
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedGT α
inst✝ : Preorder β
f g : α ≃o β
⊢ f.dual.dual = g.dual.dual

Tactic:
Subsingleton.elim f.dual

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedGT α
inst✝ : Preorder β
f g : α ≃o β
⊢ OrderIso.dual ?m.34 = g.dual.dual

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedGT α
inst✝ : Preorder β
f g : α ≃o β
⊢ αᵒᵈ ≃o βᵒᵈ
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedGT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f.dual.dual = g.dual.dual

Tactic:
Subsingleton.elim f.dual

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedGT β
inst✝ : Preorder α
f g : α ≃o β
⊢ OrderIso.dual ?m.34 = g.dual.dual

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedGT β
inst✝ : Preorder α
f g : α ≃o β
⊢ αᵒᵈ ≃o βᵒᵈ
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x✝ : α
⊢ x✝ ∈ upperBounds s

Tactic:
rw [h, upperBounds_empty]; exact mem_univ _

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n m : ℕ
⊢ IsNat n m → IsNat (↑n) m

Tactic:
rintro ⟨⟨⟩⟩; exact ⟨rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n m : ℤ
⊢ IsInt n m → IsInt (↑n) m

Tactic:
rintro ⟨⟨⟩⟩; exact ⟨rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
div_lt_iff₀ hb,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a < 1 * b ↔ a < b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a / 2 < a ↔ 0 < a

Tactic:
div_lt_iff₀ (zero_lt_two' α),

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a < a * 2 ↔ 0 < a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b ↦ a * b) '' s) (a * b)

Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl)

Goal state after:
case inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha✝ : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun b ↦ a * b) '' s) (a * b)

case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b ↦ 0 * b) '' s) (0 * b)
Module: Mathlib.Data.List.Defs

Goal state before:
pp: ⊢ @iterate = @iterateTR

Tactic:
funext α f a n

Goal state after:
α : Type u_7
f : α → α
a : α
n : ℕ
⊢ iterate f a n = iterateTR f a n
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂ ↔ l₁ ~ l₂

Tactic:
eraseIdx_of_length_le hm

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁ ~ l₂ ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
h : Injective length
x y : α
⊢ x = y

Tactic:
(suffices [x] = [y] by simpa using this)

Goal state after:
case mp
α : Type u
h : Injective length
x y : α
⊢ [x] = [y]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ (l.set i a)[j] = l[j]

Tactic:
by
  simp [h]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a * [].alternatingProd⁻¹

Tactic:
by rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]

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

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ filter p l = foldr (fun a out ↦ bif p a then a :: out else out) [] l

Tactic:
induction l <;> simp [*, filter]

Goal state after:
case cons
α : Type u
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    else foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
⊢ filter (fun x ↦ true) l = l

Tactic:
induction l <;> simp [*, filter]

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

Goal state before:
pp: α : Type u
l : List α
⊢ filter (fun x ↦ false) l = []

Tactic:
induction l <;> simp [*, filter]

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

Goal state before:
pp: p q : ℚ≥0
⊢ p < q ↔ p.num * q.den < q.num * p.den

Tactic:
← NNRat.coe_lt_coe,

Goal state after:
p q : ℚ≥0
⊢ ↑p < ↑q ↔ p.num * q.den < q.num * p.den
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0

Tactic:
by
  rcases h₂ with ⟨u, rfl⟩
  exact left_ne_zero_of_mul h₁

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

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : n ∣ b * c
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Tactic:
obtain ⟨a₁', a₂', h₁, h₂, rfl⟩ := hn h

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
a₁' a₂' : α
h₁ : a₁' ∣ b
h₂ : a₂' ∣ c
hn : IsPrimal (a₁' * a₂')
h : a₁' * a₂' ∣ b * c
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: m k : ℕ+
⊢ m.div k = if ↑m % ↑k = 0 then (↑m / ↑k).pred else ↑m / ↑k

Tactic:
dsimp [div, modDiv]
  cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl

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

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

Tactic:
divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))

Goal state after:
case neg
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 }.den ∣ b
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
ha0 : 0 < a
⊢ 0 < ↑a

Tactic:
Int.natCast_pos

Goal state after:
a : ℕ
ha0 : 0 < a
⊢ 0 < a
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:
by
  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:
by
  simp [h]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b

Tactic:
simpa only [disjoint_comm] using @sSup_disjoint_iff

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
⊢ sSup s ≤ sSup t

Tactic:
by
  rcases eq_empty_or_nonempty s with rfl | h
  · rw [csSup_empty]
    exact bot_le
  · exact csSup_le_csSup h₁ h h₂

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

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

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

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain (fun x1 x2 ↦ r ↑x1 ↑x2) (s ↓∩ t) ↔ IsChain r (s ∩ t)

Tactic:
by
  simp [IsChain, Set.Pairwise]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : x ∈ {i}
⊢ x ∈ mulSupport (mulSingle i a)

Tactic:
by rwa [mem_mulSupport, hx, mulSingle_eq_same]

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

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

Tactic:
· rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]
    conv_rhs => rw [← fract_add_floor x]
    rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
      le_sub_comm]
    norm_cast
    rwa [le_sub_one_iff, floor_lt]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x - 1 / 2 < ↑⌊x + 1 / 2⌋

Tactic:
show x - 1 / 2 = x + 1 / 2 - 1 by linarith

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x + 1 / 2 - 1 < ↑⌊x + 1 / 2⌋
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
⊢ ⌊1⌋ = 1

Tactic:
← cast_one,

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

Tactic:
← cast_one,

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * fract x = 1 ↔ ∃ n, k * x = k * ↑n + 1

Tactic:
fract,

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * (x - ↑⌊x⌋) = 1 ↔ ∃ n, k * x = k * ↑n + 1
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
⊢ fract (a + b) ≤ fract a + fract b

Tactic:
fract,

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

Tactic:
fract,

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

Tactic:
fract,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + b - ↑⌊a + b⌋ ≤ a - ↑⌊a⌋ + (b - ↑⌊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
a b : R
⊢ fract a + fract b ≤ fract (a + b) + 1

Tactic:
fract,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a - ↑⌊a⌋ + fract b ≤ fract (a + b) + 1
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 - ↑⌊a⌋ + fract b ≤ fract (a + b) + 1

Tactic:
fract,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a - ↑⌊a⌋ + (b - ↑⌊b⌋) ≤ fract (a + b) + 1
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 - ↑⌊a⌋ + (b - ↑⌊b⌋) ≤ fract (a + b) + 1

Tactic:
fract,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a - ↑⌊a⌋ + (b - ↑⌊b⌋) ≤ a + b - ↑⌊a + b⌋ + 1
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 0 = 0

Tactic:
fract,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ 0 - ↑⌊0⌋ = 0