mathlib-initiative/mathlib-tactics huggingface dataset:
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₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ Injective fun n ↦ a ^ n

Tactic:
obtain ha₁ | ha₁ := ha₁.lt_or_gt

Goal state after:
case inl
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun n ↦ a ^ n

case inr
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun n ↦ a ^ n
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f (a ⊓ b) ≤ f ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)

Tactic:
rw [pow_succ]

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ k * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [pow_succ]

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [pow_succ]

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)

Tactic:
rw [pow_succ]

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n * x
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k.succ < 1

Tactic:
rw [pow_succ]

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k * x < 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) = a ^ (n + 1) * a

Tactic:
rw [pow_succ]

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

Goal state before:
pp: a b : ℤ
H : b ≠ 0
⊢ a % b < |b|

Tactic:
rw [← emod_abs]; exact emod_lt_of_pos _ (abs_pos.2 H)

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

Tactic:
apply le_of_mul_le_of_one_le_right _ (one_le_mabs _); rw [mabs_div_sup_mul_mabs_div_inf]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ b / a = |a / b|ₘ

Tactic:
mabs_of_le_one,

Goal state after:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ b / a = (a / b)⁻¹

case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ a / b ≤ 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
h : s ≠ 0
⊢ s.gcdA 0 = 1

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h

Goal state after:
s : ℕ
h : s.succ ≠ 0
⊢ s.succ.gcdA 0 = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
h : s ≠ 0
⊢ s.gcdB 0 = 0

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h

Goal state after:
s : ℕ
h : s.succ ≠ 0
⊢ s.succ.gcdB 0 = 0
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ 0 ≤ b

Tactic:
by_contra hb

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : ¬0 ≤ b
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsLeftRegular 0 ↔ ∃ x y, x ≠ y

Tactic:
not_iff_comm,

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ IsLeftRegular 0
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsRightRegular 0 ↔ ∃ x y, x ≠ y

Tactic:
not_iff_comm,

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ IsRightRegular 0
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑(a✝ + a✝¹)

Tactic:
WithBot.coe_le_coe

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝ + a✝¹
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑(a✝¹ + a✝)

Tactic:
WithBot.coe_le_coe

Goal state after:
case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝¹ + a✝
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + b

Tactic:
tsub_add_cancel_of_le h₁

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ 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 : α
⊢ 0 < a - b ↔ ¬a ≤ b

Tactic:
pos_iff_ne_zero,

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]

Tactic:
have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one

Goal state after:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
this : -↑n < 1
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
x : WithBot α
⊢ ↑a ≤ x → x ≤ ↑a

Tactic:
cases x <;> simp; simpa using @h _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst✝ : IsReduced α
hn : n ≠ 0
⊢ 0 < a ^ n ↔ 0 < a

Tactic:
pos_iff_ne_zero,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst✝ : IsReduced α
hn : n ≠ 0
⊢ a ^ n ≠ 0 ↔ a ≠ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
z : αˣ
hz : 1 < z
⊢ y * z⁻¹ < y

Tactic:
simp [hz]

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

Goal state before:
pp: case pos.mpr
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ k + 1
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
⊢ k + 1 = m

Tactic:
rcases Decidable.lt_or_eq_of_le hle with hlt | rfl

Goal state after:
case pos.mpr.inl
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ k + 1
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
hlt : m < k + 1
⊢ k + 1 = m

case pos.mpr.inr
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
hle : k + 1 ≤ k + 1
h0 : k + 1 ≠ 0 → P (k + 1)
hm : ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ k + 1 → ¬P n
⊢ k + 1 = k + 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : LinearOrder R
inst✝⁷ : FloorSemiring R
S : Type u_3
inst✝⁶ : Semiring S
inst✝⁵ : LinearOrder S
inst✝⁴ : FloorSemiring S
F : Type u_4
inst✝³ : FunLike F R S
inst✝² : RingHomClass F R S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
by rw [← map_natCast f, hf.le_iff_le]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
F : Type u_4
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
by rw [← map_natCast f, hf.le_iff_le]

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

Goal state before:
pp: 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)
⊢ IsUnit a

Tactic:
by
    rcases eq_or_ne a 0 with (rfl | h)
    · 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
    · exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩

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

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

Tactic:
rw [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 : R
inst✝ : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k + 1) < 0

Tactic:
rw [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.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ (fun x ↦ f x.1 x.2) '' s ×ˢ t ↔ x✝ ∈ image2 f s t

Tactic:
simp [and_assoc]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ IsGreatest (f '' s) (f a) ↔ IsLeast s a

Tactic:
by
  simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
x✝ : (α × β) × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u ↔ x✝ ∈ (s ×ˢ t) ×ˢ u

Tactic:
simp [and_assoc]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u

Tactic:
simp [and_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ upperBounds s

Tactic:
by
  rw [h.upperBounds_eq]
  rfl

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

Goal state before:
pp: x y : ℕ
⊢ ¬x.ble y = true ↔ ¬x ≤ y

Tactic:
Nat.ble_eq

Goal state after:
x y : ℕ
⊢ ¬x ≤ y ↔ ¬x ≤ y
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d

Tactic:
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]

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

Goal state before:
pp: α : Type u
n : ℕ
l : List α
⊢ l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n

Tactic:
grind [cases List]

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

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

Tactic:
simp +contextual only [zpow', true_and, ite_eq_left_iff]

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ ¬n = 0 → 0 ^ n = 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f a l = a

Tactic:
foldl_fixed' hf l

Goal state after:
α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ a = a
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ ((∃ as, x₂ = x₁ ++ as ∧ (as = [] ∧ a₂ = a₁ ∧ z₂ = z₁ ∨ ∃ as', as = a₁ :: as' ∧ z₁ = as' ++ a₂ :: z₂)) ∨
      ∃ bs, x₁ = x₂ ++ bs ∧ (bs = [] ∧ a₁ = a₂ ∧ z₁ = z₂ ∨ ∃ as', bs = a₂ :: as' ∧ z₂ = as' ++ a₁ :: z₁)) →
    x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
rintro (⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩ |
      ⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩) <;> simp_all

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

Goal state before:
pp: case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
· ext; simp [toNNRat, hp, hq, mul_nonneg]

Goal state after:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q / r) = ↑q / ↑r

Tactic:
by
  rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _),
    inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: α : Type u
t : BinaryTree α
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
⊢ traverse pure t = pure t

Tactic:
by
  induction t with
  | nil => rw [traverse]
  | node v l r hl hr =>
    rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a a' b : R
p : a = a'
e : ℕ
hone : Nat.rawCast 1 = e
hb : a' ^ e * Nat.rawCast 1 = b
⊢ a = b + 0

Tactic:
simp [← hone, ← hb, *]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n)

Tactic:
apply le_antisymm <;> simp only [iSup_le_iff]

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ i ≥ n, u i ≤ ⨆ i, u (i + n)

case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ (fun i ↦ u (i + n)) (i - n) = u i

Tactic:
dsimp only

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
p : β → Prop
⊢ ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i

Tactic:
by
  simpa [Classical.em] using @iSup_union _ _ _ f { i | p i } { i | ¬p i }

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

Goal state before:
pp: α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ (⨆ i, f i) a = ⨆ i, f i a

Tactic:
rw [iSup, sSup_apply, iSup, iSup, ← image_eq_range (fun f : ∀ i, β i => f a) (range f), ←
    range_comp]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x

Tactic:
sUnion_eq_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨆ x ∈ ⋃ i, ↑i, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ x ∈ ⋃₀ S, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x

Tactic:
sUnion_eq_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ x ∈ ⋃ i, ↑i, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x
Module: Mathlib.Data.Set.Order

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ MonotoneOn f s ↔ Monotone fun a ↦ f ↑a

Tactic:
simp [Monotone, MonotoneOn]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b

Tactic:
calc
  _ ≤ ⨆ a ∈ s, a ∆ sSup t := by simpa [sSup_image] using sSup_symmDiff_le hs
  _ ≤ _ := iSup_mono fun a ↦ iSup_mono fun _ ↦ by simpa [sSup_image] using symmDiff_sSup_le ht

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (fun a ↦ f a '' t) x ⊓ (fun a ↦ f a '' t) y ⊆ ⊥

Tactic:
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
a : β
ha : a ∈ t
b : β
hb : b ∈ t
hab : f x a = f y b
⊢ f y b ∈ ⊥
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (fun b ↦ (fun a ↦ f a b) '' s) x ⊓ (fun b ↦ (fun a ↦ f a b) '' s) y ⊆ ⊥

Tactic:
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : (fun a ↦ f a x) a = (fun a ↦ f a y) b
⊢ (fun a ↦ f a y) b ∈ ⊥
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : LE A
inst✝ : IsConcreteLE A B
p q : A
⊢ ¬p ≤ q ↔ ∃ x, x ∈ p ∧ ¬x ∈ q

Tactic:
by
  simpa [← coe_subset_coe] using! Set.not_subset

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ sInf (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
  obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd
  refine hs.out B.2 c.2 ⟨?_, ?_⟩
  · exact (Subtype.mono_coe (· ∈ s)).le_csInf_image ⟨c, hct⟩ hB
  · exact (Subtype.mono_coe (· ∈ s)).csInf_image_le hct ⟨B, hB⟩

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
p q : ℚ
⊢ p < q → ↑p < ↑q

Tactic:
simpa only [sub_pos, cast_sub] using cast_pos_of_pos (K := K) (q := q - p)

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

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = (⌊2 * fract x⌋ + 1) / 2

pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
Int.floor_eq_zero_iff.mpr

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = (0 + 1) / 2

case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 2 * fract x ∈ Ico 0 1

case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case zero
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : 0 < 0
hk : (m : ℕ+) → m < ⟨0, kprop⟩ → p m
⊢ p ⟨0, kprop⟩

pp: case succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1
hk : (m : ℕ+) → m < ⟨k + 1, kprop⟩ → p m
⊢ p ⟨k + 1, kprop⟩

Tactic:
· exact (lt_irrefl 0 kprop).elim

Goal state after:
case succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1
hk : (m : ℕ+) → m < ⟨k + 1, kprop⟩ → p m
⊢ p ⟨k + 1, kprop⟩
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
hx' : 2 * x ∉ range Int.cast
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
· rw [round_eq_div, (ceil_eq_floor_add_one_iff_notMem _).mpr hx']

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
inst✝ : IsOrderedRing R
a b : R
⊢ fract a + fract b ≤ fract (a + b) + 1

Tactic:
rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋