mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c

Tactic:
exact _root_.trans h₁ h₃

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * a * a

Tactic:
rw [pow_succ, pow_two]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
a : α
b : β
⊢ (∃ h, a = cast h b) → a ≍ b

Tactic:
rintro ⟨rfl, h⟩; rw [h, cast_eq]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: case left
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α

Tactic:
exact inferInstance

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: case right
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Nonempty α

Tactic:
exact inferInstance

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ r = fun x1 x2 ↦ f x1 = x2

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩
  rcases forall_existsUnique_iff'.1 h with ⟨f, rfl : r = _⟩
  exact ⟨f, symm_apply_eq_iff.1 ‹_›, rfl⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
a b : α
h : TransGen r a b
⊢ r a b

Tactic:
induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact IsTrans.trans _ _ _ hac hcd

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : One β
inst✝ : One γ
f : α → β
g : β → γ
hg : Injective g
hg0 : g 1 = 1
⊢ g ∘ f = 1 ↔ f = 1

Tactic:
by
  simpa [hg0, const_one] using comp_eq_const_iff 1 f hg

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: case refl
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p ⋯
⊢ p ⋯

Tactic:
exact h Iff.rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ min a b = if a < b then a else b

Tactic:
rw [min_comm, min_def, ← ite_not]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then a else b) = if a < b then a else b
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
⊢ IsEquiv α (fun x1 x2 ↦ x1 ≠ x2)ᶜ

Tactic:
by
  convert! eq_isEquiv α
  simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
⊢ False

Tactic:
rcases hne.1.lt_or_gt with h₁ | h₁

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
⊢ False

case inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
⊢ False
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x

Tactic:
cases h₁ : f true <;> cases h₂ : f false <;> grind [cases Bool]

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ a, a ∈ s ∧ ¬a ∈ t

Tactic:
by
  simp only [subset_def, not_forall, exists_prop]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f (b ⊓ c)

Tactic:
map_inf

Goal state after:
α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f b ⊓ f c
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t) ∩ sᶜ ⊆ t

Tactic:
by
  simp [union_inter_distrib_right]

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t) ∩ tᶜ ⊆ s

Tactic:
by
  simp [union_inter_distrib_right]

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
rw [removeNone_none _ h]
    simpa using (congr_arg e.symm h).symm

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
⊢ a ∆ b = b \ a

Tactic:
rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅

Tactic:
image_eq_empty

Goal state after:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ s = ∅ ↔ s = ∅
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
⊢ val '' univ = s

Tactic:
simp [-image_univ, coe_image]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = univ.pi (update (fun x ↦ univ) i s)

Tactic:
by
  ext x
  simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y

Tactic:
exact congr_arg f (h H)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f (insert a s) (insert (f a) t)

Tactic:
repeat rw [insert_eq]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ ↑n = (a ^ ↑n)⁻¹

Tactic:
rw [zpow_natCast, zpow_natCast, inv_pow]

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux

Tactic:
by
  rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b) = (fun b a ↦ f a b) <$> b <*> a

Tactic:
by
      rw [@CommApplicative.commutative_prod m h]
      simp [map_seq, map_map]
      rfl

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case negSucc
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ f.subtypePerm hf ^ Int.negSucc n = (f ^ Int.negSucc n).subtypePerm ⋯

Tactic:
simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
n : ℤ
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
cases n with
  | ofNat n => exact subtypePerm_pow _ _ _
  | negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

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

Goal state before:
pp: α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * (b * a * b)

Tactic:
hb,

Goal state after:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * (1 * b)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
pow_sub_of_lt a⁻¹ h,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / b = c / d
hb : b = 0
⊢ False

Tactic:
hb,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / 0 = c / d
hb : b = 0
⊢ False
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Tactic:
by
  simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Even (a + b)

Tactic:
by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
  refine ⟨a + b + 1, ?_⟩
  rw [two_mul, two_mul]
  ac_rfl

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]
  simp

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ c⁻¹ * a ≤ b ↔ a ≤ b * c

Tactic:
inv_mul_le_iff_le_mul,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a ≤ c * b ↔ a ≤ b * c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d

Tactic:
simpa using mul_right_inj_of_comparable (le_total d b) |>.1 h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
c d : α
hcd : a * b * c ≤ a * b * d
⊢ a * (b * c) ≤ a * (b * d)

Tactic:
by rwa [← mul_assoc, ← mul_assoc]

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 + c + b * c ≤ b
⊢ 1 + a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, 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 + c + b * c ≤ b
⊢ 1 + (a + c + b * c) ≤ 1 + b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ 0 < a * a ↔ a ≠ 0

Tactic:
constructor
  · rintro h rfl
    rw [mul_zero] at h
    exact h.false
  · intro h
    rcases h.lt_or_gt with h | h
    exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Archimedean R
x : R
a✝ : Nontrivial R
⊢ ∃ n, x ≤ ↑n

Tactic:
exact (Archimedean.arch x one_pos).imp fun n h => by rwa [← nsmul_one]

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

Goal state before:
pp: case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y

Tactic:
inv_mul_le_iff_le_mul,

Goal state after:
case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ x * y
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
inv_mul_le_iff_le_mul,

Goal state after:
case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ x * z
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = |a|ₘ ^ n

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
· rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]
    exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n
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 : G
⊢ a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b

Tactic:
rw [le_mabs, or_comm, le_inv']

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

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b ≤ |a|ₘ * |b|ₘ

pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
· exact mul_le_mul' (le_mabs_self a) (le_mabs_self b)

Goal state after:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n ≤ 0 ↔ n = 0

Tactic:
le_zero

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n = 0 ↔ n = 0
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t

Tactic:
by
  obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
  rw [xgcdAux, Nat.strongRec_eq]
  rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : WithZero (Multiplicative M)
hx : x ≠ 0
⊢ exp x.log = x

Tactic:
lift x to Multiplicative M using hx

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
x : Multiplicative M
⊢ exp (↑x).log = ↑x
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x y : WithZero (Multiplicative M)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).log = x.log + y.log

Tactic:
lift x to Multiplicative M using hx

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
y : WithZero (Multiplicative M)
hy : y ≠ 0
x : Multiplicative M
⊢ (↑x * y).log = (↑x).log + y.log
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : WithZero (Multiplicative M)
hx : x ≠ 0
⊢ Multiplicative.toAdd (unzero hx) = x.log

Tactic:
lift x to Multiplicative M using hx

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
x : Multiplicative M
hx : ↑x ≠ 0
⊢ Multiplicative.toAdd (unzero hx) = (↑x).log
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : b ≤ a
⊢ ⋯.choose ≤ c ↔ a ≤ c + b

Tactic:
have := (exists_add_of_le h).choose_spec

Goal state after:
case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : b ≤ a
this : a = b + ⋯.choose
⊢ ⋯.choose ≤ c ↔ a ≤ c + b
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ 0 < findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
Nat.pos_iff_ne_zero,

Goal state after:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k ≠ 0 ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
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
a b : R
h : a ≤ b
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
obtain ha | ha := le_total a 0

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
obtain ha | ha := le_total a 0

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
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
a : R
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
obtain ha | ha := le_total a 0

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
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
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
obtain ha | ha := le_total a 0

Goal state after:
case 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 : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

case 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
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case 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 : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ + n = ⌈a⌉₊

Tactic:
rw [← ceil_add_natCast, tsub_add_cancel_of_le hna]

Goal state after:
case inr.ha
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 : ℕ
hna : ↑n ≤ a
⊢ 0 ≤ a - ↑n
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ ⅟(a + b) = ⅟a + ⅟b ↔ ⅟(a + b) * (a + b) = (⅟a + ⅟b) * (a + b)

Tactic:
rw [mul_left_inj_of_invertible]

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
h_b_ainv_b : -(a + b) = b * ⅟a * b
⊢ -(b + a) = b * ⅟a * b

Tactic:
← h_b_ainv_b,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
h_b_ainv_b : -(a + b) = b * ⅟a * b
⊢ -(b + a) = -(a + b)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Ring α
a : α
h : |a| = a
⊢ Odd |a| ↔ Odd a

Tactic:
simp only [h, odd_neg]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Ring α
a : α
h : |a| = -a
⊢ Odd |a| ↔ Odd a

Tactic:
simp only [h, odd_neg]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inl
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a b : β
IH : ∀ (y : β), y < b → f y = g y
hb : g b = f b
⊢ f b = g b

Tactic:
rw [hb]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : g a < g b
⊢ f a = g a

Tactic:
hb,

Goal state after:
case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : g a < f a
⊢ f a = g a
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁ l₂

Tactic:
by
      rw [← reverse_reverse l₁, ← reverse_reverse l₂]
      exact rel_reverse h

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

Goal state before:
pp: α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
⊢ n < l.length + 1

Tactic:
Nat.lt_succ_iff

Goal state after:
α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
⊢ n ≤ l.length
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < ((r, x) ::ᵣ l).eval

Tactic:
unfold eval cons
  apply mul_pos ?_ hl
  simp only
  rw [zpow'_of_ne_zero_left _ _ hx.ne']
  apply zpow_pos hx

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

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
x : M
⊢ x = eval [(1, x)]

Tactic:
simp [eval]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ l[idxOf a l]? = some a

Tactic:
getElem?_eq_getElem (idxOf_lt_length_iff.2 h),

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ some l[idxOf a l] = some a
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ ↑x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
rw [Rat.zpow_natCast, Rat.zpow_natCast, Rat.pow_succ]

Goal state after: