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

Goal state before:
pp: M : Type u_1
inst✝ : Group M
a : M
m n : ℤ
⊢ a ^ m.gcd n = 1 ↔ a ^ m = 1 ∧ a ^ n = 1

Tactic:
obtain m | m := m <;> obtain n | n := n

Goal state after:
case ofNat.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1

case ofNat.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1

case negSucc.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1

case negSucc.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1
Module: Mathlib.Algebra.Regular.Basic

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

Tactic:
pow_succ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ LeftInverse (fun x ↦ unzero ⋯) fun x ↦ unzero ⋯

Tactic:
by intro; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ RightInverse (fun x ↦ unzero ⋯) fun x ↦ unzero ⋯

Tactic:
by intro; simp

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
hx : x ≠ ⊤
⊢ y < z → x + y < x + z

Tactic:
by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

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 : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ False

Tactic:
rw [← h, tsub_pos_iff_lt] at h₁

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False
Module: Mathlib.Algebra.Order.Sub.Basic

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

Tactic:
exact (tsub_add_tsub_comm h h).symm

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 : ℤ
⊢ ↑|a| = |↑a|

Tactic:
by simp [abs_eq_max_neg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a : Additive αᵒᵈ
⊢ ⊤ + a = ⊤

Tactic:
ext; simp [bot_eq_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ -⊤ = ⊤

Tactic:
ext; simp [bot_eq_zero]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
hx : x ≠ ⊥
⊢ y < z → x + y < x + z

Tactic:
by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : a = ↑(ofAdd b)
⊢ toAdd (unzero h) = b

Tactic:
by subst k; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
⊢ MulLeftReflectLT (WithZero α)

Tactic:
refine ⟨fun a b c h => ?_⟩
  have := h.ne_zero
  induction a
  · simp at this
  induction c
  · simp at this
  induction b
  exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]

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

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

Tactic:
rw [← add_one_le_iff, le_floor]

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ↑(z + 1) ≤ a ↔ ↑z + 1 ≤ a
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
· intro a b hab
    obtain ⟨c, hc⟩ := exists_between (WithTop.coe_lt_coe.mpr hab)
    induction c with
    | top => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ n ≤ FloorSemiring.floor a ↔ n ≤ FloorSemiring.floor a

Tactic:
H₁.gc_floor,

Goal state after:
case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ ↑n ≤ a ↔ n ≤ FloorSemiring.floor a

case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

Tactic:
cases x <;> cases y <;> simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Goal state after:
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)
⊢ ⅟(a + b) = ⅟a + ⅟b ↔ ⅟(a + b) * (a + b) = (⅟a + ⅟b) * (a + b)

Tactic:
by rw [mul_left_inj_of_invertible]

Goal state after:
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)
⊢ -2 + 1 = -2 + 2 + ⅟b * a + ⅟a * b ↔ -2 + 1 = ⅟b * a + ⅟a * b

Tactic:
neg_add_cancel,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -2 + 1 = 0 + ⅟b * a + ⅟a * b ↔ -2 + 1 = ⅟b * a + ⅟a * b
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
h : IsUnit (f 0)
⊢ IsUnit 0

pp: case inr
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h✝ : IsUnit (f a)
h : a ≠ 0
⊢ IsUnit a

Tactic:
· obtain ⟨t, ht⟩ := hf
      refine (ht ?_).elim
      have := map_mul f t 0
      rw [← one_mul (f (t * 0)), mul_zero] at this
      exact (h.mul_right_cancel this).symm

Goal state after:
case inr
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h✝ : IsUnit (f a)
h : a ≠ 0
⊢ IsUnit a
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 : ℕ
⊢ (a + b) ^ (n + 2) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
pow_succ

Goal state after:
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 : ℕ
⊢ (a + b) ^ (n + 1) * (a + b) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
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
n : ℕ
⊢ (2 * (a ^ 2 + b ^ 2)) ^ n = 2 ^ n * (a ^ 2 + b ^ 2) ^ n

Tactic:
Commute.mul_pow

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ 2 ^ n * (a ^ 2 + b ^ 2) ^ n = 2 ^ n * (a ^ 2 + b ^ 2) ^ n

case h
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ Commute 2 (a ^ 2 + b ^ 2)
Module: Mathlib.Algebra.Order.Ring.Basic

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

Tactic:
pow_succ

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k) * a < 0
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ (↑u).natAbs * (↑u⁻¹).natAbs = 1

Tactic:
rw [← natAbs_mul, Units.mul_inv]; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: n : ℕ
⊢ IsUnit ↑n ↔ IsUnit n

Tactic:
simp [isUnit_iff_natAbs_eq]

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

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
pow_succ

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ n * a = a ^ n * a
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ (Set.image2 f s t).Subsingleton

Tactic:
← image_prod

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ ((fun x ↦ f x.1 x.2) '' s ×ˢ t).Subsingleton
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
⊢ ∃ n, ¬r (f (n + 1)) (f n)

Tactic:
by_contra! hf

Goal state after:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ (Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inr ⟨↑x, ⋯⟩)

Tactic:
simp only [apply_symm_apply, sumDiffSubset_apply_inr]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a k a' : α
h : a + k = a'
⊢ termg n x a + k = termg n x a'

Tactic:
by
  simp [h.symm, termg, add_assoc]

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
congr; apply Subsingleton.elim

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
congr; apply Subsingleton.elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Forall₂ r ∘r Perm = Perm ∘r Forall₂ r

Tactic:
by
  funext l₁ l₃; apply propext
  constructor
  · intro h
    rcases h with ⟨l₂, h₁₂, h₂₃⟩
    have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
    rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩
    exact ⟨l', h₂.symm, h₁.flip⟩
  · exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃

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

Goal state before:
pp: α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?

Tactic:
rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]

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:
rw [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.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ x = 1 ↔ y = 1

Tactic:
← conj_eq_one_iff (a := a) (b := x),

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ a * x * a⁻¹ = 1 ↔ y = 1
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d

Tactic:
by rw [mul_right_comm, mul_left_inj' hc]

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩

Goal state after:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩

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

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * r = s
⊢ s.num * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den = (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑s.den

Tactic:
← Rat.eq_iff_mul_eq_mul,

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * r = s
⊢ s = ↑(q.num * r.num) / ↑(↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩

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 = { num := n, den := d, den_nz := h, reduced := c }
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ f '' ({0} ∪ range succ) = range f

Tactic:
zero_union_range_succ,

Goal state after:
α : Type u_1
f : ℕ → α
⊢ f '' univ = range f
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
x✝ : BddAbove (l '' s)
x : β
hx : x ∈ upperBounds (l '' s)
⊢ u x ∈ upperBounds s

Tactic:
gc.upperBounds_l_image

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
x✝ : BddAbove (l '' s)
x : β
hx : x ∈ u ⁻¹' upperBounds s
⊢ u x ∈ upperBounds s
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
⊢ u b ∈ upperBounds s

Tactic:
gc.upperBounds_l_image

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ u ⁻¹' upperBounds s
⊢ u b ∈ upperBounds s
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
a₁ a₂ : α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ IsLUB (l '' {a₁, a₂}) (l a₁ ⊔ l a₂)

Tactic:
simp only [image_pair, isLUB_pair]

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

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j

Tactic:
mem_iUnion

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)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) ↔ x ∈ ⋃ x, C x

Tactic:
mem_iUnion

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) ↔ ∃ i, x ∈ C i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:

Tactic:
⨅ l, f (I l)
    _ ≤ f (I k) ⊓ f (I j) := le_inf (iInf_le _ _) (iInf_le _ _)
    _ = ⊥ := (h hk).eq_bot
    _ ≤ _ := bot_le

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = Ioo a b ∪ Ioo b a

Tactic:
rcases lt_or_ge a b with h | h

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ uIoo a b = Ioo a b ∪ Ioo b a

case inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo a b ∪ Ioo b a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo a b ∪ Ioo b a

Tactic:
simp [uIoo_of_ge, h]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : Nonempty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
· simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ
⊢ ↑|q| = |↑q|

Tactic:
by simp [abs_eq_max_neg]

Goal state after:
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑k = ↑k * ↑n / ↑n

Tactic:
mul_div_cancel_right₀ _ hn

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑k = ↑k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!

pp: case inr
i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
· rw [← Nat.add_assoc]
    apply Nat.le_of_lt
    apply add_factorial_succ_lt_factorial_add_succ
    assumption

Goal state after:
case inr
i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
apply Nat.mul_left_cancel (n - m).factorial_pos
    rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]

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

Goal state before:
pp: case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ↑⌊a⌋ < a

Tactic:
exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))

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
⊢ a < c ^ 0 ∧ c ^ 0 < b

Tactic:
zpow_zero

Goal state after:
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
⊢ a < 1 ∧ 1 < b
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) < y * ↑n

Tactic:
refine ⟨(lt_div_iff₀ n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ ↑(z + 1) < y * ↑n
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs

Tactic:
· generalize hm : a ::ₘ as = m
    intro h
    induction h generalizing as with
    | zero => simp at hm
    | @cons a' b as' bs ha'b h ih =>
      rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
      · exact ⟨b, bs, ha'b, h, rfl⟩
      · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

Goal state after:
case mpr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
L : List (List α)
⊢ L.flatten.Nodup ↔ (∀ (l : List α), l ∈ L → l.Nodup) ∧ Pairwise Disjoint L

Tactic:
by
  simp only [Nodup, pairwise_flatten, disjoint_left.symm, forall_mem_ne]

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

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a : α
x✝ : a ∈ l₁
b b' : σ a
h : ⟨a, b⟩ = ⟨a, b'⟩
⊢ b = b'

Tactic:
injection h with _ h

Goal state after: