mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ ∃ k, Xor (n = 2 * k) (n = 2 * k + 1)

Tactic:
rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩) <;>
  · use k
    grind

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

Goal state before:
pp: s : ℕ
⊢ gcdB 0 s = 1

Tactic:
by
  rw [gcdB, xgcd, xgcdAux, Nat.strongRec_eq]

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

Goal state before:
pp: x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)

Tactic:
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]

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

Goal state before:
pp: case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑(n * (n.gcdA k % ↑k).toNat) % ↑k = ↑(↑n * n.gcdA k % ↑k).toNat

Tactic:
Int.natCast_mul,

Goal state after:
case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑n * ↑(n.gcdA k % ↑k).toNat % ↑k = ↑(↑n * n.gcdA k % ↑k).toNat
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, ↑(a.gcd b * (n / a.gcd b)) = a * x + b * y

Tactic:
Int.natCast_mul,

Goal state after:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, ↑(a.gcd b) * ↑(n / a.gcd b) = a * x + b * y
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr.inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) = -b + -a

Tactic:
exact left_neg_eq_right_neg (a := a + b) (by simp [neg_add_cancel_of_ne_top, *])
        (by simp [add_assoc, add_neg_cancel_of_ne_top, add_neg_cancel_left_of_ne_top, *])

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₘ + n = Nat.find hₙ

Tactic:
refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_
  · have hnm : n ≤ m := le_trans hn (find_le hpm)
    refine Nat.add_le_of_le_sub hnm (find_le ?_)
    rwa [Nat.sub_add_cancel hnm]
  · rw [← Nat.sub_le_iff_le_add]
    refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_
    rw [Nat.sub_le_iff_le_add]
    exact find_le hpm

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a ≤ ↑(ofAdd b)
⊢ toAdd (unzero ha) ≤ b

Tactic:
rwa [← coe_unzero ha, coe_le_coe, ← toAdd_le, toAdd_ofAdd] at h

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌈a⌉ ≤ ↑n ↔ a ≤ ↑n

Tactic:
Int.ceil_le,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ a ≤ ↑↑n ↔ a ≤ ↑n
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
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ a * ↑n ≤ 0

Tactic:
apply mul_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a = f b

Tactic:
obtain ⟨c, hc, hac, hbc⟩ := hs _ ha _ hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
⊢ a * ⅟b * a = b * ⅟a * b

Tactic:
have h' := neg_one_eq_invOf_mul_add_invOf_mul_iff.mp h

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
⊢ a * ⅟b * a = b * ⅟a * b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
⊢ a * ⅟b * a = b * ⅟a * b

Tactic:
by
  have h' := neg_one_eq_invOf_mul_add_invOf_mul_iff.mp h
  have h_a_binv_a : -(b + a) = a * ⅟b * a := neg_add_eq_mul_invOf_mul_same_iff.mpr h'
  have h_b_ainv_b : -(a + b) = b * ⅟a * b := by
    rw [add_comm] at h'
    exact neg_add_eq_mul_invOf_mul_same_iff.mpr h'
  rw [← h_a_binv_a, ← h_b_ainv_b, add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ f (EquivLike.inv f a₁) ∣ f b ∧ f (EquivLike.inv f a₂) ∣ f c ∧ a = EquivLike.inv f a₁ * EquivLike.inv f a₂

Tactic:
EquivLike.apply_inv_apply,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ a₁ ∣ f b ∧ a₂ ∣ f c ∧ a = EquivLike.inv f a₁ * EquivLike.inv f a₂
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a - a / 2 = a / 2

Tactic:
rw [sub_eq_iff_eq_add, add_halves]

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

Goal state before:
pp: case inr.inr
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
⊢ (fun a ↦ a ^ n) a + (c ^ n + d ^ n) < (fun a ↦ a ^ n) b + (c ^ n + d ^ n)

Tactic:
dsimp

Goal state after:
case inr.inr
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
⊢ a ^ n + (c ^ n + d ^ n) < b ^ n + (c ^ n + d ^ n)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
⊢ f ↑q = f (↑q.num / ↑q.den)

Tactic:
by rw [ratCast, div, intCast, natCast, Rat.cast_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (a : α), a ∈ s → (fun b ↦ f a b) '' t ⊆ u

Tactic:
image2_subset_iff,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → (fun b ↦ f a b) '' t ⊆ u
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (b : β), b ∈ t → (fun a ↦ f a b) '' s ⊆ u

Tactic:
image2_subset_iff,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → (fun a ↦ f a b) '' s ⊆ u
Module: Mathlib.Data.Set.NAry

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

Tactic:
image_image2,

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ image2 (fun a b ↦ g (f a b)) s t = image2 f' (g₁ '' s) (g₂ '' t)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ^ 0 = b ^ 0 ↔ 0 = 0 ∨ a = b ∨ a = -b ∧ Even 0

Tactic:
simp [pow_eq_pow_iff_of_ne_zero, *]

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

Goal state before:
pp: case inr
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
simp [pow_eq_pow_iff_of_ne_zero, *]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddAbove t → BddAbove (image2 f s t)

Tactic:
by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b ⊆ insert a s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Tactic:
insert_eq_of_mem ha,

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {a b : Set (α ⊕ β)},
    { toFun := fun s ↦ (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s), invFun := fun s ↦ Sum.inl '' s.1 ∪ Sum.inr '' s.2, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun s ↦ (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s), invFun := fun s ↦ Sum.inl '' s.1 ∪ Sum.inr '' s.2,
            left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ⊆ b

Tactic:
by simp [subset_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ IsGreatest univ a ↔ IsTop a

Tactic:
simp [IsGreatest, mem_upperBounds, IsTop]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x a : α
⊢ term 0 x a = a

Tactic:
simp [term, zero_nsmul]

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

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

Tactic:
funext α f a n
  exact Eq.symm <| iterateTR_loop_eq f a n []

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

pp: case neg
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
· have : q b := by rwa [← hpq h₁]
      simp only [filter_cons_of_pos h, filter_cons_of_pos this, forall₂_cons, h₁, true_and,
        rel_filter hpq h₂]

Goal state after:
case neg
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ l⁻¹.eval = l.eval⁻¹

Tactic:
by
  simp +instances only [NF.eval, List.map_map, NF.instInv, List.prod_inv]
  congr! 2
  ext p
  simp [zpow'_neg]

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

Goal state before:
pp: q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num ^ n).natAbs.Coprime (den ^ n)

Tactic:
Int.natAbs_pow

Goal state after:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num.natAbs ^ n).Coprime (den ^ n)
Module: Mathlib.Data.Rat.Defs

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

Tactic:
by rw [divInt_eq_div]

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

Goal state before:
pp: p q : ℚ≥0
a b : ℕ
hab : ↑a = ↑b
⊢ a = b

Tactic:
by simpa using! congr_arg num hab

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:
rw [← NNRat.coe_lt_coe, Rat.lt_iff]

Goal state after:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den < (↑q).num * ↑(↑p).den ↔ p.num * q.den < q.num * p.den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Tactic:
← Rat.num_nonneg

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn✝ : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }.num
e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩
⊢ ↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩ = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ ↑(num ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) /
      ↑(den ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) =
    ↑a / ↑b

Tactic:
dsimp

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ ↑n / ↑d = ↑a / ↑b
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.num * q.num) / ↑(p.den * q.den) = ↑p.num / ↑p.den * (↑q.num / ↑q.den)

pp: case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0

Tactic:
(Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b) = c.mul c

Tactic:
by simp [two_mul, pow_add, ← h1]

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
t : BinaryTree α
⊢ map (g ∘ f) t = map g (map f t)

Tactic:
by
  induction t with
  | nil => rw [map, map, map]
  | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 - e2) = t1 - t2

Tactic:
simp [left_distrib, *, sub_eq_add_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c

Tactic:
subst_vars; rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]

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

Goal state before:
pp: ⊢ {0} ∪ range succ = univ

Tactic:
by
  ext n
  cases n <;> simp

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

Goal state before:
pp: case e'_4
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = ((fun n ↦ rec x f n) ∘ succ) x✝

Tactic:
dsimp

Goal state after:
case e'_4
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = f x✝ (rec x f x✝)
Module: Mathlib.Order.GaloisConnection.Basic

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

Tactic:
dsimp

Goal state after:
α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
a : α
inst✝ : Nonempty ι
⊢ ⨆ x, a = a

Tactic:
rw [iSup, range_const, sSup_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
⊢ (⋃ y, range fun x ↦ ↑(f x y)) = ⋃ x, C x

Tactic:
by
  ext x; rw [mem_iUnion, mem_iUnion]; constructor
  · rintro ⟨y, i, rfl⟩
    exact ⟨i, (f i y).2⟩
  · rintro ⟨i, hx⟩
    obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩
    exact ⟨y, i, congr_arg Subtype.val hy⟩

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
⊢ (⋃ x ∈ univ.pi s, univ.pi fun a ↦ t a (x a)) = univ.pi fun a ↦ ⋃ j ∈ s a, t a j

Tactic:
ext
  simp [Classical.skolem, forall_and]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ sSup s ∆ a ≤ sSup ((fun x ↦ x ∆ a) '' s)

Tactic:
rw [sSup_image', sSup_eq_iSup']

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ (⨆ a, ↑a) ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with
    ⟨z', mem5, H3, H4⟩

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
z' : α
mem5 : z' ∈ s
H3 : r z z'
H4 : r c z'
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
have ⟨a, ha⟩ := exists_ne (0 : α)
  obtain lt | lt := ha.lt_or_gt
  · exact ⟨0, ⟨-a, neg_nonneg.mpr lt.le⟩, Subtype.coe_ne_coe.mp (neg_ne_zero.mpr ha).symm⟩
  · exact ⟨0, ⟨a, lt.le⟩, Subtype.coe_ne_coe.mp ha.symm⟩

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
⊢ sInf ∅ = default

Tactic:
simp [sInf]

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

Tactic:
rw [oneLePart_def, sup_mul, one_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel, sup_assoc,
    ← sup_assoc a, sup_eq_right.2 le_sup_right]

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

Goal state before:
pp: case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ k.descFactorial (n + 1) ≤ m.descFactorial (n + 1)

Tactic:
rw [descFactorial_succ, descFactorial_succ]
    exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

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

Goal state before:
pp: n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ (n + 1).recOn one succ = succ n (n.recOn one succ)

Tactic:
by
  obtain ⟨n, h⟩ := n
  cases n <;> [exact absurd h (by decide); rfl]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ ↑(round x) ≤ x + 1 / 2

Tactic:
rw [round_eq x]
  exact Int.floor_le (x + 1 / 2)

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

Goal state before:
pp: n : ℤ
d : ℕ
⊢ ⌈↑n / ↑d⌉ = -(-n / ↑d)

Tactic:
by
  conv_lhs => rw [← neg_neg ⌈_⌉, ← floor_neg]
  rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]

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

Goal state before:
pp: q : ℚ
⊢ q.num < (⌊q⌋ + 1) * ↑q.den

Tactic:
by
  suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den from mod_cast this
  suffices (q.num : ℚ) < (q - fract q + 1) * q.den by
    have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
    rwa [this]
  suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den by
    have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
      calc
        (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp
    rwa [this]
  suffices 0 < (1 - fract q) * q.den by
    rw [← sub_lt_iff_lt_add']
    simpa
  have : 0 < 1 - fract q := by
    have : fract q < 1 := fract_lt_one q
    have : 0 + fract q < 1 := by simp [this]
    rwa [lt_sub_iff_add_lt]
  exact mul_pos this (by exact mod_cast q.pos)

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ (q_inv - ↑⌊q_inv⌋).num < q.num

Tactic:
suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num by
    simp only [gt_iff_lt, q_inv]
    field_simp
    simp [q_inv, this]

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
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
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋

Tactic:
simp [floor_lt]

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
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ⌈a⌉

Tactic:
← Int.ceil_toNat,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉.toNat = ⌈a⌉