mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  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
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)

Tactic:
by
  rw [IsRightRegular, ← mul_right_iterate]
  exact rra.iterate n

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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ f (↑x * ↑x⁻¹) = 0

Tactic:
map_mul,

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ f ↑x * f ↑x⁻¹ = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z)

Tactic:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using fun _ ↦ by gcongr

Goal state after:
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 : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b

Tactic:
rw [← tsub_add_cancel_of_le hca]

Goal state after:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - c + c - b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
ext x
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z)

Tactic:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: case coe.zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ + 0 ≤ ↑a✝ + c

pp: case coe.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + c

Tactic:
· rw [add_zero]
    induction c
    · rw [add_zero]
    · rw [← coe_add, coe_le_coe]
      exact le_add_of_nonneg_right (h _)

Goal state after:
case coe.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝² : Add α
inst✝¹ : Add β
inst✝ : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
ext x
  simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ ↑a ≤ b ↔ a ≤ id b

Tactic:
Int.cast_id,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ a ≤ b ↔ a ≤ id b
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ id a ≤ b ↔ a ≤ ↑b

Tactic:
Int.cast_id,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ id a ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Floor.Defs

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

Tactic:
rw [← FloorRing.intCast_strictMono.le_iff_le (β := α), Int.cast_zero]
  exact (floor_le a).trans ha

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

pp: case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

pp: case inr.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Tactic:
· obtain ⟨w, hws, hwr⟩ := ha y hy
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Goal state after:
case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

case inr.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ f (↑a * ↑a⁻¹) = 0

Tactic:
map_mul,

Goal state after:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ f ↑a * f ↑a⁻¹ = 0
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₂
⊢ a₁ * a₂ = f (EquivLike.inv f a₁ * EquivLike.inv f a₂)

Tactic:
map_mul,

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₁ * a₂ = f (EquivLike.inv f a₁) * f (EquivLike.inv f a₂)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a / b + c * b / (b * d)

Tactic:
hbd.eq,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a / b + c * b / (d * b)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: 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) = d ^ n

Tactic:
rw [← add_assoc, hn.pow_add_pow_eq_zero hac.symm, zero_add]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - c * b) / c

Tactic:
simpa using div_sub_div a b hc one_ne_zero

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

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y

Tactic:
· have := hφ (ψts ys) (ψts xs) ψyx
    rw [φψs.eq ys, φψs.eq xs] at this
    induction le_antisymm l this
    exact le_refl _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s' t
⊢ f a b ∈ image2 f (s \ s') t

Tactic:
exact ⟨_, ⟨ha, fun ha' ↦ h ⟨_, ha', _, hb, rfl⟩⟩, _, hb, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ ∀ (x : α), x ∈ Icc a a ↔ x ∈ {a}

Tactic:
simp [Icc, le_antisymm_iff, and_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Icc a b \ {a} ↔ x ∈ Ioc a b

Tactic:
simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

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

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n

Tactic:
induction n generalizing a l <;> simp [*]

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

Goal state before:
pp: x y : ℕ
⊢ x.ble y = false ↔ y < x

Tactic:
by
  rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 < a / b ↔ a < b

Tactic:
lt_div_iff_of_neg hb,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a < 1 * b ↔ a < b
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b c : α
⊢ a = b ∨ a ∈ [c] ↔ a = b ∨ a = c

Tactic:
mem_singleton

Goal state after:
α : Type u
a b c : α
⊢ a = b ∨ a = c ↔ a = b ∨ a = c
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a : α
⊢ count a l = count a (filter (fun b ↦ decide (P b)) l) + count a (filter (fun x ↦ decide ¬P x) l)

Tactic:
by
  unfold count
  convert countP_eq_countP_filter_add l _ P
  simp only [decide_not]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ [y]

Tactic:
mem_singleton

Goal state after:
α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x = y
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
rw [hf a' ha' mem_cons_self, one_mul, add_zero]

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

Goal state before:
pp: α : Type u
l : List α
f : α → Bool
⊢ l.length = (filter f l).length + (filter (fun x ↦ !f x) l).length

Tactic:
simp_rw [← List.countP_eq_length_filter, l.length_eq_countP_add_countP f, Bool.not_eq_true,
    Bool.decide_eq_false]

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

Goal state before:
pp: q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁ * n₂).natAbs.Coprime (d₁ * d₂)

Tactic:
rw [Int.natAbs_mul]; exact (hnd₁.mul_left h₂₁).mul_right (h₁₂.mul_left hnd₂)

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

Goal state before:
pp: p : ℚ
q : ℚ≥0
hq : 0 < q
hp : p < 0
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
by
    simp only [(hp.trans_le q.coe_nonneg).not_ge, toNNRat_eq_zero.2 hp.le, hq.not_ge]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
hx0 : x = 0
⊢ False

Tactic:
by simp [hx0] at hyx

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

Goal state before:
pp: case eq
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n

Tactic:
simp only [Int.ofNat_eq_natCast, Int.cast_neg,
    Int.cast_natCast, invOf_eq_inv, inv_neg, neg_mul, mul_inv_rev, inv_inv]

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f (↑r.num * (↑r.den)⁻¹) = g (↑r.num * (↑r.den)⁻¹)

Tactic:
map_mul,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f ↑r.num * f (↑r.den)⁻¹ = g (↑r.num * (↑r.den)⁻¹)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f ↑r.num * f (↑r.den)⁻¹ = g (↑r.num * (↑r.den)⁻¹)

Tactic:
map_mul,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f ↑r.num * f (↑r.den)⁻¹ = g ↑r.num * g (↑r.den)⁻¹
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f (↑r.num * (↑r.den)⁻¹) = g (↑r.num * (↑r.den)⁻¹)

Tactic:
map_mul,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f ↑r.num * f (↑r.den)⁻¹ = g (↑r.num * (↑r.den)⁻¹)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f ↑r.num * f (↑r.den)⁻¹ = g (↑r.num * (↑r.den)⁻¹)

Tactic:
map_mul,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f ↑r.num * f (↑r.den)⁻¹ = g ↑r.num * g (↑r.den)⁻¹
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteSemilatticeSup α
a : α
s : ι → α
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
by
  simp [iSup, le_sSup_iff, upperBounds]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b

Tactic:
by
    split_ifs with h
    · simp [h]
    · simp [(CompleteLinearOrder.le_total a b).resolve_left h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a

Tactic:
by
    split_ifs with h
    · simp [h]
    · simp [(CompleteLinearOrder.le_total a b).resolve_left h]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set α
x : α
hx : x ∈ ⋃ i, s i
⊢ Nonempty ι

Tactic:
exact ⟨Classical.choose <| mem_iUnion.mp hx⟩

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤
    ⨆ i,
      ⨅ j,
        match i, j with
        | { down := true }, j => a
        | { down := false }, j => ↑j

Tactic:
by
        simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
a b c : α
⊢ a ⇨ b ≤ c ↔ ∀ (d : α), d ⊓ a ≤ b → d ≤ c

Tactic:
simp [himp_eq_sSup]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : b < sSup s
⊢ ∃ a ∈ s, b < a

Tactic:
contrapose! hb

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : ∀ a ∈ s, a ≤ b
⊢ sSup s ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ IsGLB (f '' Icc a b) (f a)

Tactic:
refine isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ≤ f a → b' ∈ lowerBounds (f '' Icc a b)

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simpa only [uIcc_comm a] using eq_of_mem_uIcc_of_mem_uIcc

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : b ≤ a
hb : b ≤ c
⊢ b = c

Tactic:
refine hb.eq_of_not_lt fun hc => ?_

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : b ≤ a
hb : b ≤ c
hc : b < c
⊢ False
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨i, j, h⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i < j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨i, j, h⟩

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddAbove t
h : sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) = ↑(sSup t)

Tactic:
simp [h, h', h'']

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddBelow t
h : sInf (Subtype.val '' t) ∈ s
⊢ sInf (Subtype.val '' t) = ↑(sInf t)

Tactic:
simp [h, h', h'']

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

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

Tactic:
obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ∈ s
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r / ↑b' + q = q

Tactic:
rw [Int.ediv_eq_zero_of_lt, zero_add]

Goal state after:
case H1
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ 0 ≤ ↑r

case H2
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r < ↑b'
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = ↑q'

Tactic:
Int.cast_id,

Goal state after:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = q'
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb; infer_instance

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb; infer_instance

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb; infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ⊓ b = a / (a / b)⁺ᵐ

Tactic:
by
  simp [oneLePart, div_sup, inf_comm]

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb; infer_instance

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

Goal state before:
pp: case zero.zero
k : ℕ
⊢ ascFactorial 0 0 * (0 + 0).ascFactorial k = ascFactorial 0 (0 + k)

Tactic:
simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) ≤ f x + f y

Tactic:
rw [div_eq_mul_inv, ← map_inv_eq_map f y]

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x * y⁻¹) ≤ f x + f y⁻¹
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑↑q = ↑q

Tactic:
by
  rw [Rat.cast_def, NNRat.cast_def, NNRat.cast_def]
  have hn := @num_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
  on_goal 1 => have hd := @den_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
  case hdp => simpa only [Int.natCast_pos] using q.den_pos
  simp only [Int.cast_natCast, Nat.cast_inj] at hn hd
  rw [hn, hd, Int.cast_natCast]

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

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

Tactic:
floor_intCast_div_natCast

Goal state after:
n : ℤ
d : ℕ
⊢ -(-n / ↑d) = -(-n / ↑d)