mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

Tactic:
by
  by_cases h' : n.bit b = 0
  case pos =>
    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
    simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h
    unfold binaryRec
    exact h.symm
  case neg =>
    rw [binaryRec, dif_neg h']
    change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
    generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
⊢ bit b n h
      (binaryRec zero
        (fun b n ih ↦
          if h : n = 0 → b = true then bit b n h ih
          else
            have this := ⋯;
            ⋯ ▸ zero)
        n) =
    bit b n h (binaryRec' zero bit n)

Tactic:
binaryRec'

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
⊢ bit b n h
      (binaryRec zero
        (fun b n ih ↦
          if h : n = 0 → b = true then bit b n h ih
          else
            have this := ⋯;
            ⋯ ▸ zero)
        n) =
    bit b n h
      (binaryRec zero
        (fun b n ih ↦
          if h : n = 0 → b = true then bit b n h ih
          else
            have this := ⋯;
            ⋯ ▸ zero)
        n)
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
h : ∀ (x y : α), (x == y) = (x == y)
⊢ inst1 = inst2

Tactic:
by
  have ⟨beq1⟩ := inst1
  congr
  funext x y
  exact h x y

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen r ≤ ReflTransGen r

Tactic:
intro a _ h

Goal state after:
α : Type u_1
r : α → α → Prop
a i✝ : α
h : TransGen r a i✝
⊢ ReflTransGen r a i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b

case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x y : α
⊢ TransGen (ReflGen r) x y ↔ ReflTransGen r x y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y

case refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (SymmGen r) = EqvGen r

Tactic:
← eqvGen_eq_reflTransGen,

Goal state after:
α : Type u_1
r : α → α → Prop
⊢ EqvGen (SymmGen r) = EqvGen r
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ (Equiv.refl α).trans e = e

Tactic:
by cases e; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ map id id a = a

Tactic:
map_id,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ id a = a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.lt ↔ b ≤ a

Tactic:
cases h : compare a b
  · simpa using compare_lt_iff_lt.1 h
  · simpa using le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h
  · simpa using le_of_lt <| compare_gt_iff_gt.1 h

Goal state after:
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:
convert! eq_isEquiv α
  simp [compl]

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

Tactic:
simp only [subset_def, not_imp_not]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Lattice α
a b c : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c

Tactic:
rintro ⟨rfl, rfl⟩
    exact ⟨inf_idem _, sup_idem _⟩

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
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
a b : α
⊢ f b ≤ f a ⊔ f b

Tactic:
exact le_sup_right

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

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

Tactic:
bot_sdiff

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y

Tactic:
sup_inf_self,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ (y ⊔ y ⊓ x) = y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ (y ⊔ y ⊓ x) = y

Tactic:
sup_inf_self,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ y = y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)

Tactic:
sup_inf_self,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
⊢ LeftInverse (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val)

Tactic:
rintro (⟨x, hx⟩ | ⟨x, hx⟩) <;> dsimp

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inl ⟨x, hx⟩

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inr ⟨x, hx⟩
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : extend f g j (f x) = extend f g j (f y)
⊢ f x = f y

Tactic:
rw [hf.extend_apply, hf.extend_apply] at heq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : g x = g y
⊢ f x = f y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
by
  simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_or]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (fun a ↦ ↑a) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val ⁻¹' s = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s

Tactic:
MapsTo.restrict_commutes,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f ∘ Subtype.val '' Subtype.val ⁻¹' s = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Function.diag '' s = Function.diag '' Function.diag ⁻¹' s ×ˢ s

Tactic:
diag_preimage_prod_self

Goal state after:
α : Type u_1
s : Set α
⊢ Function.diag '' s = Function.diag '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f univ univ ↔ Bijective f

Tactic:
simp [Bijective, BijOn]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : M →* G
a b : M
⊢ (f (a * b))⁻¹ = (f a)⁻¹ * (f b)⁻¹

Tactic:
simp_rw [← mul_inv, f.map_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1 ^ Int.negSucc n = 1

Tactic:
rw [zpow_negSucc, one_pow, inv_one]

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

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
| pred n ih =>

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

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
zpow_sub_one

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n) * g⁻¹)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
| pred n ih =>

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a / b = c / b * (a / c)

Tactic:
simp [mul_left_comm c]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

Tactic:
← div_eq_inv_mul,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = d⁻¹ * c ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = d⁻¹ * c ↔ a * d = c * b

Tactic:
← div_eq_inv_mul,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ ↑((liftRight f g h) x)⁻¹ * f x = 1

Tactic:
by
  rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
← mul_left_cancel_iff (a := a),

Goal state after:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ a * (b * a) = a * 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

Tactic:
← div_eq_inv_mul,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = d⁻¹ * c ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = d⁻¹ * c ↔ a * d = c * b

Tactic:
← div_eq_inv_mul,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑(1 + n) = 1 + ↑n

Tactic:
rw [Nat.cast_add, Nat.cast_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 2 + 1 = 3

Tactic:
rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]
  apply congrArg
  decide

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Tactic:
by rw [div_eq_mul_inv, mul_self_mul_inv a]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a

Tactic:
by
    rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg,
      ← Int.natCast_succ, zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc,
      inv_mul_cancel₀ ha, mul_one]

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑(m + 1) = ↑(n✝ + 1)
⊢ m + 1 = n✝ + 1

Tactic:
simp only [Nat.cast_succ, add_right_cancel_iff] at h

Goal state after:
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑m = ↑n✝
⊢ m + 1 = n✝ + 1
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M₂ →+ M
hf : Injective ⇑f
smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x
c₁ c₂ : R
x : M₂
⊢ f ((c₁ + c₂) • x) = f (c₁ • x + c₂ • x)

Tactic:
simp only [smul, f.map_add, add_smul]

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

Goal state before:
pp: case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
· rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]

Goal state after:
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:
rw [hb, div_zero] at h

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

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
m n : ℤ
⊢ ↑m = ↑n ↔ m = n

Tactic:
by rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
⊢ q • 1 = ↑q

Tactic:
NNRat.smul_def,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
⊢ ↑q * 1 = ↑q
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
inst✝ : NonAssocSemiring α
⊢ (Set.range fun x ↦ 2 * x) = {a | Even a}

Tactic:
by
  ext x
  simp [eq_comm, two_mul, Even]

Goal state after:
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
⊢ 0 = b ^ 2 + a * b

Tactic:
rw [sq, ← add_mul, add_comm, hab, zero_mul]

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

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

Tactic:
inv_lt_inv_iff

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ c < b ↔ c < b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a

Tactic:
exact le_of_lt this

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 b c : G₀
hc : 0 < c
⊢ a ≤ b / c ↔ a * c ≤ b

Tactic:
rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]

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 b c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ a * c < b

Tactic:
lt_mul_inv_iff₀ hc

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c < b ↔ a * c < 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 : ℕ
⊢ 1 ≤ ↑n ↔ 1 ≤ n

Tactic:
rw [← cast_one, cast_le]

Goal state after:
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 ≤ 1 ↔ n ≤ 1

Tactic:
rw [← cast_one, cast_le]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ (∃ c, b = a * c) ∧ a ≠ b ↔ ∃ c, c > 1 ∧ b = a * c

Tactic:
← exists_and_right

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]; exact .of_mul

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

Goal state before:
pp: case refine_1.zero
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
hab : (map' f) 0 = ↑b
⊢ ∃ a, f a = b

Tactic:
simp at hab

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

Goal state before:
pp: case refine_1.coe
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a✝ : α
hab : (map' f) ↑a✝ = ↑b
⊢ ∃ a, f a = b

Tactic:
simp at hab

Goal state after:
case refine_1.coe
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a✝ : α
hab : f a✝ = b
⊢ ∃ a, f a = b
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 α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c

Tactic:
← add_tsub_cancel_of_le h,

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

Tactic:
by
  rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right h₂]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m

Tactic:
simp only [← not_lt, find_lt_iff, not_exists, not_and]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∃ x, ↑a < x ∧ p x) ↔ ∃ b, a < b ∧ p ↑b

Tactic:
by
  simp [WithBot.exists]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∃ x, ↑a ≤ x ∧ p x) ↔ ∃ b, a ≤ b ∧ p ↑b

Tactic:
by
  simp [WithBot.exists]

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
x : α
n : ℕ
hn : -x ≤ ↑n
⊢ ∃ n, ↑n ≤ x

Tactic:
use -n

Goal state after:
case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
x : α
n : ℕ
hn : -x ≤ ↑n
⊢ ↑(-↑n) ≤ x
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ DirectedOn r (Set.range f) ↔ Directed r f

Tactic:
by
  simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]

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₀
hx : a ≠ 0
H : f a = 0
⊢ False

Tactic:
lift a to G₀ˣ using isUnit_iff_ne_zero.mpr hx

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
⊢ False
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
by
      by_cases h : a = 0
      · rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
      · rw [zpow_add_one₀ h]

Goal state after: