mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f (f a b) c = f b (f a c)

Tactic:
hc.comm a,

Goal state after:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f (f b a) c = f b (f a c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
m✝ n✝ m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
simp [*, parity_simps]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b : α
inst✝ : AddLeftMono α
h : a ≤ b
c : α
⊢ c ≤ b + (c - a)

Tactic:
← h,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b : α
inst✝ : AddLeftMono α
h : a ≤ b
c : α
⊢ c ≤ a + (c - a)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
⊢ a * (a⁻¹ * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : 0 ≤ b
⊢ 0 * (0⁻¹ * b) ≤ b

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
ha : a ≠ 0
⊢ a * (a⁻¹ * b) ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
⊢ b ≤ a * (a⁻¹ * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : b ≤ 0
⊢ b ≤ 0 * (0⁻¹ * b)

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
ha : a ≠ 0
⊢ b ≤ a * (a⁻¹ * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
⊢ a⁻¹ * (a * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : 0 ≤ b
⊢ 0⁻¹ * (0 * b) ≤ b

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
ha : a ≠ 0
⊢ a⁻¹ * (a * b) ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
⊢ b ≤ a⁻¹ * (a * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : b ≤ 0
⊢ b ≤ 0⁻¹ * (0 * b)

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
ha : a ≠ 0
⊢ b ≤ a⁻¹ * (a * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
⊢ a / a ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
⊢ 0 / 0 ≤ 1

case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a / a ≤ 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
⊢ a⁻¹ * a ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
⊢ 0⁻¹ * 0 ≤ 1

case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ * a ≤ 1
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₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
by simpa using one_le_inv_mul₀ ha (b := 1)

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c⁻¹ * b
⊢ c * a ≤ b

Tactic:
obtain rfl | hc := hc.eq_or_lt
  · simpa using hb
  · rwa [le_inv_mul_iff₀ hc] at h

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
⊢ ¬0 < a ∨ ¬a ≤ 1 ↔ a ≤ 0 ∨ ¬a ≤ 1

Tactic:
not_lt

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < a ∧ b < 0 ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
neg_lt_zero

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ c⁻¹ * b ↔ a * c ≤ b

Tactic:
rw [le_inv_mul_iff₀ hc, mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r ↪r s
h : (fun x ↦ x.toFun) f = (fun x ↦ x.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r ↪r s
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s ({ toFun := toFun✝, inj' := inj'✝ } a) ({ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h : (fun x ↦ x.toFun) { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ } = (fun x ↦ x.toFun) g
⊢ { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ } = g
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ cmp (f (g x✝)) x✝ = Ordering.eq

Tactic:
← h,

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ cmp (g x✝) (g x✝) = Ordering.eq
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered Y → DenselyOrdered X

Tactic:
· intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)
    exact ⟨EquivLike.inv f c, by simpa using hc⟩

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ |a / b|ₘ ≤ n

Tactic:
by
  rw [mabs_div_le_iff, div_le_iff_le_mul, div_le_iff_le_mul]
  exact ⟨le_mul_of_le_of_one_le a_le_n one_le_b, le_mul_of_le_of_one_le b_le_n one_le_a⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ -(a / -[n+1]) = -0

Tactic:
rw [← Int.ediv_neg]

Goal state after:
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ a / - -[n+1] = -0
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⟩)

Goal state after:
case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Mul R
a : R
ca : ∀ (b : R), Commute a b
h : IsRightRegular a
⊢ IsLeftRegular a

Tactic:
simp only [@Commute.symm_iff R _ a] at ca
  exact fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
ua : IsUnit a
⊢ IsRegular a

Tactic:
by
  rcases ua with ⟨a, rfl⟩
  exact Units.isRegular a

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:
← h,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ ⦃x : Additive αᵒᵈ⦄, x ≠ ⊤ → x + -x = 0

Tactic:
by
    simp +contextual [bot_eq_zero, Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
      -ofDual_eq_zero]

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

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
by
  classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
  exact ⟨lb, H⟩

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 : toAdd (unzero ha) < b
⊢ a < ↑(ofAdd b)

Tactic:
rwa [← coe_unzero ha, coe_lt_coe, ← ofAdd_toAdd (unzero ha), ofAdd_lt]

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑⌈a⌉

Tactic:
exact ha.trans (le_ceil a)

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

Goal state before:
pp: case inr.inr
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 : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ + n = ⌊a⌋₊

Tactic:
← floor_add_natCast _,

Goal state after:
case inr.inr
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 : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n + ↑n⌋₊ = ⌊a⌋₊

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 : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n
Module: Mathlib.Order.WithBot

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

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

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

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ a * b = 1

Tactic:
← h,

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ a * ⅟a = 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ b * a = 1

Tactic:
← h,

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ ⅟a * a = 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b

Tactic:
by
  apply invOf_eq_right_inv
  rw [h, mul_invOf_self]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - ↑⌈a⌉₊| ≤ 1

Tactic:
by
  refine abs_le.mpr ⟨?_, ?_⟩
  · simpa using (ceil_lt_add_one ha).le
  · simpa using (le_ceil a).trans (le_add_of_nonneg_left zero_le_one)

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

Goal state before:
pp: case mk
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₂ : FloorSemiring R
floor✝ ceil✝ : R → ℕ
floor_of_neg✝ : ∀ {a : R}, a < 0 → floor✝ a = 0
gc_floor✝ : ∀ {a : R} {n : ℕ}, 0 ≤ a → (n ≤ floor✝ a ↔ ↑n ≤ a)
gc_ceil✝ : GaloisConnection ceil✝ Nat.cast
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ { floor := floor✝, ceil := ceil✝, floor_of_neg := floor_of_neg✝, gc_floor := gc_floor✝, gc_ceil := gc_ceil✝ } = H₂

Tactic:
cases H₂

Goal state after:
case mk.mk
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
floor✝¹ ceil✝¹ : R → ℕ
floor_of_neg✝¹ : ∀ {a : R}, a < 0 → floor✝¹ a = 0
gc_floor✝¹ : ∀ {a : R} {n : ℕ}, 0 ≤ a → (n ≤ floor✝¹ a ↔ ↑n ≤ a)
gc_ceil✝¹ : GaloisConnection ceil✝¹ Nat.cast
floor✝ ceil✝ : R → ℕ
floor_of_neg✝ : ∀ {a : R}, a < 0 → floor✝ a = 0
gc_floor✝ : ∀ {a : R} {n : ℕ}, 0 ≤ a → (n ≤ floor✝ a ↔ ↑n ≤ a)
gc_ceil✝ : GaloisConnection ceil✝ Nat.cast
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ { floor := floor✝¹, ceil := ceil✝¹, floor_of_neg := floor_of_neg✝¹, gc_floor := gc_floor✝¹, gc_ceil := gc_ceil✝¹ } =
    { floor := floor✝, ceil := ceil✝, floor_of_neg := floor_of_neg✝, gc_floor := gc_floor✝, gc_ceil := gc_ceil✝ }
Module: Mathlib.Algebra.GroupWithZero.Invertible

Goal state before:
pp: α : Type u
inst✝² : MulZeroOneClass α
a : α
inst✝¹ : Nontrivial α
inst✝ : Invertible a
ha : a = 0
⊢ 0 = ⅟a * a

Tactic:
by simp [ha]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Equiv

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
x✝ : G₀
⊢ (fun x ↦ x * a) ((fun x ↦ x / a) x✝) = x✝

Tactic:
by simp [ha]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Equiv

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
x✝ : G₀
⊢ (fun x ↦ x / a) ((fun x ↦ x * a) x✝) = x✝

Tactic:
by simp [ha]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Equiv

Goal state before:
pp: G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
x✝ : G₀
⊢ (fun x ↦ a / x) ((fun x ↦ a / x) x✝) = x✝

Tactic:
by simp [ha]

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

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

Tactic:
rw [← natAbs_mul, Units.inv_mul]

Goal state after:
u : ℤˣ
⊢ natAbs 1 = 1
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
K : Type u_1
inst✝ : DivisionRing K
⊢ 0⁻¹ = 0 ↔ 0 = -1 ∨ 0 = 0 ∨ 0 = 1

case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
by
  obtain n0 | n0 := le_total 0 n
  · obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
    simp only [mabs_pow, zpow_natCast, Nat.abs_cast]
  · obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
    rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]
    exact mabs_pow m _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
⊢ f a '' t = t

Tactic:
show f a = id from funext h,

Goal state after:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
⊢ id '' t = t
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
s : Set α
⊢ f '' upperBounds s ⊆ upperBounds (f '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩
  exact Hf.mem_upperBounds_image ha

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

Tactic:
by
  refine ⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩
  · grind [h.wf.has_min, trichotomous_of r]
  · grind [wellFounded_iff_has_min]
  · grind [h {a, b} <| by simp]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a x : α
⊢ x ∈ Iic a \ {a} ↔ x ∈ Iio a

Tactic:
by simp [lt_iff_le_and_ne]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioc x y)
a : α
ha : a ∈ Ioc x y
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
by
    rcases exists_between ha.1 with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, mem_Ioc.mpr ⟨hb₁, hb₂.le.trans ha.2⟩⟩, hb₂⟩

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

Goal state before:
pp: α : 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
⊢ q b = true

Tactic:
← hpq h₁

Goal state after:
α : 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
⊢ p a = true
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : 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
⊢ ¬q b = true

Tactic:
← hpq h₁

Goal state after:
α : 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
⊢ ¬p a = true
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case hab
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ max |q| |r| ≤ B + 1

Tactic:
refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)

Goal state after:
case hab
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q| ≤ B + 1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b : α
n : ℕ
⊢ a = b ↔ n + 1 = 0 ∨ a = b

Tactic:
by simp only [n.succ_ne_zero, false_or]

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
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
rw [hm]

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (0 * n) = zpow' (zpow' a 0) n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
s t : List α
x : α
h : x ∈ s.head?
⊢ x ∈ (s ++ t).head?

Tactic:
grind [Option.mem_def]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
p : ℤ × M
l : NF M
⊢ (p ::ᵣ l).eval = l.eval * zpow' p.2 p.1

Tactic:
by
  unfold eval cons
  simp [mul_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = l'.eval * zpow' (n, e).2 (n, e).1

Tactic:
← h,

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = L.eval * l.eval * zpow' (n, e).2 (n, e).1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Tactic:
· intro ⟨h₁, h₂⟩
    exact ext_get h₁ h₂

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod * (drop l'.length l).prod * (drop l.length l').prod =
    (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod

Tactic:
← h,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod * (drop l.length l).prod * (drop l.length l').prod =
    (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod
Module: Mathlib.Data.Rat.Defs

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

Tactic:
divInt_eq_div

Goal state after:
n d : ℤ
⊢ ↑n / ↑d = ↑n / ↑d
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
Rat.le_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.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
cast_divInt_of_ne_zero _ (by simpa),

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑n₁ / ↑↑d₁ = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
a : α
⊢ Commute (↑q) a

Tactic:
simpa only [cast_def] using (q.num.cast_commute a).div_left (q.den.cast_commute a)

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

Goal state before:
pp: n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝

Tactic:
exact ⟨_, h⟩

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

Goal state before:
pp: n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝

Tactic:
exact ⟨_, h⟩

Goal state after: