mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: case inr
m n : ℕ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one n with h₂ | h₂

Goal state after:
case inr.inl
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inr
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n✝ : ℕ
a✝ : a ^ n✝ ∣ b ^ n✝
⊢ a ^ (n✝ + 1) ∣ b ^ (n✝ + 1)

Tactic:
rw [pow_succ, pow_succ]
    gcongr

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ n • a + a = a * ↑(n + 1)

Tactic:
ih,

Goal state after:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ a * ↑n + a = a * ↑(n + 1)
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + (f (x * y) - f x * f y - f x * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero (M₀ := α),
        sub_eq_zero, or_iff_not_imp_left] at hxy

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : ¬2 = 0 → f (x * y) = f x * f y
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ * r⁻¹ʳ ^ n = r⁻¹ʳ * (r ^ n)⁻¹ʳ

Tactic:
Ring.inverse_pow r n

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ * (r ^ n)⁻¹ʳ = r⁻¹ʳ * (r ^ n)⁻¹ʳ
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑n • b + b = n • b + 1 • b

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ n • b + b = n • b + 1 • b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2) ↔
    (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2

Tactic:
refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 < x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 < x2) b c

case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 = x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 = x2) b c

case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
ih,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ 0 * a ^ 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
by
  rcases lt_trichotomy a 0 with (ha | rfl | ha)
  · refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonpos_of_nonneg ha.le hb
  · rw [zero_mul] at hab
    exact hab.false.elim
  · refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonneg_of_nonpos ha.le hb

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + (a + b + b * c) ≤ 1 + c
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₀
⊢ 0 < a⁻¹ ↔ 0 < a

Tactic:
suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
⊢ ∀ (a : G₀), 0 < a → 0 < a⁻¹
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩

Tactic:
by
    intro x y
    dsimp only
    split_ifs <;> simp [Subtype.ext_iff]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
⊢ 0 < a⁻¹ ↔ 0 < a

Tactic:
suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
⊢ ∀ (a : G₀), 0 < a → 0 < a⁻¹
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ a * b ≤ max a c * max d b

Tactic:
by simpa [mul_comm, max_comm] using ba

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₀
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

Tactic:
simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]

Goal state after:
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₀
ha : 0 < a
hc : 0 < c
⊢ a < b / c ↔ c < b / a

Tactic:
rw [lt_div_iff₀ ha, lt_div_iff₀' hc]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝) b

Tactic:
cases b

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝¹ val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝¹ : α₁
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝) b

Tactic:
cases b

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝¹ : α₂
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝¹ val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * (a ⊔ a⁻¹)

Tactic:
mul_sup,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a ⊔ (a ⊔ a⁻¹) * a⁻¹
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]

Goal state after:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ 1 ≤ a / b
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
⊢ ∃ c x, a * c = b

Tactic:
by
  obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
  refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩
  rintro rfl
  simp [hc] at h

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

Goal state before:
pp: case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1

pp: case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ n = 1

Tactic:
· rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]

Goal state after:
case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ n = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (a ^ m ∈ Set.range fun x ↦ x ^ n) ↔ a ∈ Set.range fun x ↦ x ^ n

Tactic:
simp [pow_eq_pow_iff_of_coprime hmn.symm]; aesop

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
d : α
x y : WithOne α
⊢ unoneD d x = unoneD d y ↔ x = y ∨ x = ↑d ∧ y = 1 ∨ x = 1 ∧ y = ↑d

Tactic:
by
  induction y <;> simp [unoneD_eq_iff, or_comm]

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

Goal state before:
pp: case top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
b : WithTop G
⊢ ⊤ - b = ⊤ + -b

Tactic:
cases b

Goal state after:
case top.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
⊢ ⊤ - ⊤ = ⊤ + -⊤

case top.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ + -↑a✝
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
b : WithTop G
a✝ : G
⊢ ↑a✝ - b = ↑a✝ + -b

Tactic:
cases b

Goal state after:
case coe.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ↑a✝ - ⊤ = ↑a✝ + -⊤

case coe.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ↑a✝¹ + -↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b : WithTop α
a c : α
h : ↑a ≤ ↑(a + c)
⊢ ∃ c_1, ↑(a + c) = ↑a + c_1

Tactic:
exact ⟨c, rfl⟩

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

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

Tactic:
have hnm : n ≤ m := le_trans hn (find_le hpm)

Goal state after:
case refine_1
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₘ + n
hpm : p m
hnm : n ≤ m
⊢ Nat.find hₘ + n ≤ m
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ c : α
h : ↑a✝ ≤ ↑(a✝ + c)
⊢ ∃ c_1, ↑(a✝ + c) = ↑a✝ + c_1

Tactic:
exact ⟨c, rfl⟩

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
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ ⌈↑n⌉₊ ≤ a ↔ n ≤ a

Tactic:
by rw [ceil_le, cast_le]

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

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

Tactic:
rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
    exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
x y z : WithTop α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← WithTop.coe_inf, ← WithTop.coe_sup]
    simpa [← coe_inf, ← coe_sup] using le_sup_inf

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n k : α
hkm : m ≤ k
hkn : n ≤ k
⊢ f m ≤ g n

Tactic:
calc
    f m ≤ f k := hf hkm
    _ ≤ g k := h _
    _ ≤ g n := hg hkn

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) ↔ DenselyOrdered α

Tactic:
constructor <;> intro h <;> constructor
  · 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⟩
  · simpa [WithTop.exists, WithTop.forall, exists_gt] using DenselyOrdered.dense

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : WithBot α
⊢ a < b ↔ ∃ x, ↑x < b ∧ a < ↑x

Tactic:
rw [lt_iff_exists_coe_btwn]; simp_rw [and_comm]

Goal state after:
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₀
⊢ f a ≠ 0 ↔ a ≠ 0

Tactic:
refine ⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, ?_⟩

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₀
⊢ a ≠ 0 → f a ≠ 0
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ -(b - c) ↔ a ∣ c - b

Tactic:
neg_sub

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ c - b ↔ a ∣ c - b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
refine lt_of_add_lt_add_right (a := c ^ n + d ^ n) ?_

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ (fun a ↦ a ^ n) a + (c ^ n + d ^ n) < (fun a ↦ a ^ n) b + (c ^ n + d ^ n)
Module: Mathlib.Algebra.Field.Basic

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

Tactic:
simpa using div_sub_div b a one_ne_zero hc

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
⊢ image2 f {a} t ∪ image2 f s t = (fun b ↦ f a b) '' t ∪ image2 f s t

Tactic:
image2_singleton_left

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
⊢ f a '' t ∪ image2 f s t = (fun b ↦ f a b) '' t ∪ image2 f s t
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|

Tactic:
simpa only [sq_abs] using sq_le_sq₀ (abs_nonneg a) (abs_nonneg b)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range fun x ↦ g (f x))

Tactic:
change BddAbove (range (g ∘ f))

Goal state after:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range (g ∘ f))
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}

Tactic:
by
  rw [← Icc_sdiff_right, sdiff_sdiff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
⊢ MapsTo (Sum.elim f g) (sumEquiv.symm s) t

Tactic:
by
  rintro (a | b) <;> aesop

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a - b = c

Tactic:
by
  rw [sub_eq_add_neg, h]

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

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a : M
⊢ (replicate 0 a).prod = 1

Tactic:
replicate_zero,

Goal state after:
case zero
M : Type u_2
inst✝ : Monoid M
a : M
⊢ [].prod = 1
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ a * (replicate n a).prod = a ^ (n + 1)

Tactic:
ih,

Goal state after:
case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ a * a ^ n = a ^ (n + 1)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
⊢ ∃ c, 0 < c ∧ b * c < a

Tactic:
by
  have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one))
  refine ⟨a / max (b + 1) 1, this, ?_⟩
  rw [← lt_div_iff₀ this, div_div_cancel₀ h.ne']
  exact lt_max_iff.2 (Or.inl <| lt_add_one _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
H : Forall₂ R [] l
⊢ l = []

Tactic:
cases H; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
H : Forall₂ R l []
⊢ l = []

Tactic:
cases H; rfl

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
⊢ l.prod = (map id l).prod

Tactic:
rw [map_id]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * xs.prod * (y * ys.prod) =
    x * y * (zipWith (fun x1 x2 ↦ x1 * x2) xs ys).prod * (drop (y :: ys).length (x :: xs)).prod *
      (drop (x :: xs).length (y :: ys)).prod

Tactic:
conv =>

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| (zipWith (fun x1 x2 ↦ x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod