mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n / 2 = n

Tactic:
rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]

Goal state after:
b : Bool
n : Nat
⊢ b.toNat < 2

case H
b : Bool
n : Nat
⊢ 0 < 2
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a

Tactic:
rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 2 → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : k + 2 ≠ 0
⊢ m * npowRec' (k + 2) m = npowRec' (k + 2) m * m

Tactic:
simp [npowRec', ← mul_assoc, ih]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : h
⊢ p h

Tactic:
simpa only [H]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : ¬h
⊢ p h

Tactic:
simpa only [H]

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
this : (fun x ↦ c) = fun x ↦ if x = b₀ then c' else c
⊢ c = c'

pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ ((fun g ↦ g ∘ f) fun x ↦ c) = (fun g ↦ g ∘ f) fun x ↦ if x = b₀ then c' else c

Tactic:
· simpa using congr_fun this b₀

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ ((fun g ↦ g ∘ f) fun x ↦ c) = (fun g ↦ g ∘ f) fun x ↦ if x = b₀ then c' else c
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
hinj : Injective f
⊢ (Relation.Map r f f on f) = r

Tactic:
ext x y
  exact ⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · cases h with
    | refl => exact Or.inl rfl
    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)
  · rcases h with (rfl | h)
    · rfl
    · exact h.to_reflTransGen

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower M P Q
h : Surjective fun m ↦ m • 1
n : N
p : P
q : Q
⊢ (n • p) • q = n • p • q

Tactic:
obtain ⟨m, rfl⟩ := h n

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower M P Q
h : Surjective fun m ↦ m • 1
p : P
q : Q
m : M
⊢ ((fun m ↦ m • 1) m • p) • q = (fun m ↦ m • 1) m • p • q
Module: Mathlib.Logic.Pairwise

Goal state before:
pp: n : ℕ
R : Fin n.succ → Fin n.succ → Prop
inst✝ : Std.Symm R
⊢ Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun i j ↦ R i.succ j.succ

Tactic:
by
  simp only [pairwise_fin_succ_iff, comm (b := 0) (r := R), and_self_left]

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

Goal state before:
pp: case false.false
h : false ≤ false
⊢ false.toNat ≤ false.toNat

Tactic:
simp_all +decide

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

Goal state before:
pp: case false.true
h : false ≤ true
⊢ false.toNat ≤ true.toNat

Tactic:
simp_all +decide

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

Goal state before:
pp: case true.false
h : true ≤ false
⊢ true.toNat ≤ false.toNat

Tactic:
simp_all +decide

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

Goal state before:
pp: case true.true
h : true ≤ true
⊢ true.toNat ≤ true.toNat

Tactic:
simp_all +decide

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

Goal state before:
pp: a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a * b ≤ a ^ b

Tactic:
cases b with

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

Goal state before:
pp: k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 * k ^ 2 + 2 * k ^ 2 = (2 * k) ^ 2

Tactic:
by rw [Nat.mul_pow, ← Nat.add_mul]

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

Goal state before:
pp: f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : c < f N
⊢ f N = c + 1

Tactic:
specialize hc N

Goal state after:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hc : f N ≤ c + 1
hN : c < f N
⊢ f N = c + 1
Module: Mathlib.Order.Lattice

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Lattice α
b : α
⊢ b ⊓ b = b ∧ b ⊔ b = b

Tactic:
exact ⟨inf_idem _, sup_idem _⟩

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (e₁ x) = pure (e₂ x)

Tactic:
simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x)

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ x ⊔ y \ x

Tactic:
sup_sdiff_cancel_right hx

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ∆ (a \ b) = a ⊔ b

Tactic:
symmDiff_sdiff_eq_sup,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ⊔ a = a ⊔ b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Injective ((Membership.mem ∘ preimage f) ∘ ofPred) ↔ Surjective f

Tactic:
exact injective_comp_right_iff_surjective

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
⊢ Surjective (codRestrict f (range f) ⋯)

Tactic:
rintro ⟨b, ⟨a, rfl⟩⟩
  exact ⟨a, rfl⟩

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b = a ↔ b = 1

Tactic:
mul_eq_left

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
⊢ b = 1 ↔ b = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * (u₁.inv * ↑u₁ * ↑u₂) = 1

Tactic:
inv_val,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * (1 * ↑u₂) = 1
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ LawfulFunctor (Sum e)

Tactic:
constructor <;> intros

Goal state after:
case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

case id_map
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝

case comp_map
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
h : 1 < n
⊢ n < n * n

Tactic:
have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h)

Goal state after:
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n m : ℕ
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m

Tactic:
← Nat.exists_mul_self m,

Goal state after:
m✝ n m : ℕ
⊢ IsSquare m ↔ ∃ n, n * n = m
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: a b : Prop
l : List Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: l)
h_last : l.getLastD b → a
⊢ (a :: b :: l).TFAE

Tactic:
induction l generalizing a b with
  | nil => simp_all [tfae_cons_cons, iff_def]
  | cons c l IH =>
    simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
    rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
    have := IH ⟨bc, ch⟩ (ab ∘ h_last)
    exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
m : ℕ
⊢ ↑(m * 0) = ↑m * ↑0

Tactic:
simp [mul_add, *]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
m n✝ : ℕ
a✝ : ↑(m * n✝) = ↑m * ↑n✝
⊢ ↑(m * (n✝ + 1)) = ↑m * ↑(n✝ + 1)

Tactic:
simp [mul_add, *]

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
have hxy := h (x + y)

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f ((x + y) * (x + y)) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ x⁻¹ʳ * (x * z) = z

Tactic:
inverse_mul_cancel_left _ _ h

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ z = z
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c

Tactic:
mul_assoc d,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = d * b * d⁻¹ * c ↔ d * a = b * c

Tactic:
mul_assoc d,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = d * (b * d⁻¹) * c ↔ d * a = b * c
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ (a + -b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b

Tactic:
add_sq',

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + (-b) ^ 2 + 2 * a * -b = a ^ 2 + b ^ 2 - 2 * a * b
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ 2 ∣ a

Tactic:
simp [Even, Dvd.dvd, two_mul]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2
a : α
ha✝ : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ b * a ≤ c * a

Tactic:
exact @CovariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

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

Goal state before:
pp: M₀ : Type u_2
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ a * b < c * d

Tactic:
rw [← b0, mul_zero]

Goal state after:
M₀ : Type u_2
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 < a
⊢ StrictMono fun n ↦ a ^ n

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one₀ (zero_lt_one.trans ha).ne']
  exact lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

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

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ a ≠ 0 → 0 < a * a

Tactic:
· intro h
    rcases h.lt_or_gt with h | h
    exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]

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

Goal state before:
pp: α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
by
    rw [← mul_le_mul_iff_left (x ⊓ (y ⊓ z)), inf_mul_sup x (y ⊓ z), ← inv_mul_le_iff_le_mul,
      le_inf_iff]
    constructor
    · rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]
      exact mul_le_mul' (inf_le_inf_left _ inf_le_left) inf_le_left
    · rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
      exact mul_le_mul' (inf_le_inf_left _ inf_le_right) inf_le_right

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n < 1 ↔ n = 0

Tactic:
Nat.lt_succ_iff,

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n ≤ 0 ↔ n = 0
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + -a = 0 ↔ a ≠ ⊤

Tactic:
add_neg_cancel_iff_ne_top

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a ≠ ⊤ ↔ a ≠ ⊤
Module: Mathlib.Algebra.Order.Sub.Basic

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

Tactic:
rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ ↑a ≤ -↑1

Tactic:
← Int.cast_neg,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ ↑a ≤ ↑(-1)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case none
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), none ≤ ↑a → x ≤ ↑a) ↔ x ≤ none

Tactic:
simp [WithBot.none_eq_bot, eq_bot_iff_forall_le]

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

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

Tactic:
div_self h

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ -1 = -1
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * (x - y) + (a - b) * y

Tactic:
rw [mul_sub_left_distrib, mul_sub_right_distrib]

Goal state after:
α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * x - a * y + (a * y - b * y)
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ image2 f s t \ image2 f s' t ⊆ image2 f (s \ s') t

Tactic:
by
  rintro - ⟨⟨a, ha, b, hb, rfl⟩, h⟩
  exact ⟨_, ⟨ha, fun ha' ↦ h ⟨_, ha', _, hb, rfl⟩⟩, _, hb, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoTopOrder α
⊢ ¬BddAbove univ

Tactic:
by simp [BddAbove]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ IsLUB s a ↔ IsLUB s b

Tactic:
by
  simp [isLUB_iff_le_iff, h.le_congr_left]

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

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e

Tactic:
have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d

Goal state after:
A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
⊢ 0 < e
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:
rw [div_le_iff₀ (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: γ : Type u_1
⊢ LawfulFunctor (Const γ)

Tactic:
constructor <;> intros

Goal state after:
case map_const
γ : Type u_1
α✝ β✝ : Type u_2
⊢ mapConst = map ∘ Function.const β✝

case id_map
γ : Type u_1
α✝ : Type u_2
x✝ : Const γ α✝
⊢ id <$> x✝ = x✝

case comp_map
γ : Type u_1
α✝ β✝ γ✝ : Type u_2
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const γ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a + (b - a) / 2 < b

Tactic:
rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]

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

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : (a :: l₁).length = (b :: l₂).length
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)

Tactic:
simp only [length_cons, succ.injEq] at h₁
        exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
x✝² : List α
x✝¹ : List β
x✝ : Forall₂ R x✝² x✝¹
⊢ Forall₂ R (take 0 x✝²) (take 0 x✝¹)

Tactic:
simp only [Forall₂.nil, take]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
n✝ : ℕ
⊢ Forall₂ R (take (n✝ + 1) []) (take (n✝ + 1) [])

Tactic:
simp only [Forall₂.nil, take]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ = ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Tactic:
← forall₂_comp_perm_eq_perm_comp_forall₂,

Goal state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Forall₂ r ∘r Perm) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.head? = l.head?

Tactic:
by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
  induction l <;> simp [replicate]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
simp [zpow', ha]
    by_cases hn : n = 0
    · simp +contextual [hn, zero_zpow]
    · simp +contextual [hn, zero_zpow]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = a / a

Tactic:
simp [zpow']
  by_cases h : a = 0
  · simp [h]
  · simp [h]

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

Goal state before:
pp: l : List ℤ
n : ℤ
⊢ l.sum % n = (map (fun x ↦ x % n) l).sum % n

Tactic:
by
  induction l <;> simp [Int.add_emod, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b

Tactic:
constructor
  · rintro rfl
    exact hnd (dvd_zero _)
  · rcases hd with ⟨c, rfl⟩
    refine ⟨c, ?_, rfl⟩
    rintro ⟨u, rfl⟩
    simp at hnd

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

Goal state before:
pp: q : ℚ
n : ℤ
⊢ (q + -↑n).den = q.den

Tactic:
← Int.cast_neg,

Goal state after:
q : ℚ
n : ℤ
⊢ (q + ↑(-n)).den = q.den
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ¬p.den = 0

Tactic:
apply den_ne_zero

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ¬q.den = 0

Tactic:
apply den_ne_zero

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

Tactic:
apply den_ne_zero

Goal state after:
case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ¬p.den = 0

Tactic:
apply den_ne_zero

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ¬q.den = 0

Tactic:
apply den_ne_zero

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑(a * ↑d) = ↑(n * b)
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b

Tactic:
rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: α : Type u
x : BinaryTree α
⊢ 0 < x.numNodes + 1

Tactic:
exact x.numNodes.zero_lt_succ

Goal state after: