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

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

Tactic:
by
  rcases trichotomous_of r a b with (h₃ | rfl | h₃)
  · exact _root_.trans h₃ h₂
  · exact h₂
  · exact absurd h₃ h₁

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

Goal state before:
pp: M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
this : one₁ = one₂
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ } =
    { one := one₂, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }

Tactic:
cases this

Goal state after:
case refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ } =
    { one := one₁, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by
    apply inv_eq_of_mul
    rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ b = c

Tactic:
rw [← mul_inv_cancel_right b a, show b * a = c * a from h, mul_inv_cancel_right]

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a * (b * a⁻¹) = b

Tactic:
rw [mul_comm, inv_mul_cancel_right]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = c

Tactic:
by rw [← h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
b : α
A : P → α
⊢ (dite P A fun x ↦ b) ≠ b ↔ ∃ h, A h ≠ b

Tactic:
simp only [Ne, dite_eq_right_iff, not_forall]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
fab : α → β
fbc : β → γ
ga : α → α
gb : β → β
gc : γ → γ
hab : Semiconj fab ga gb
hbc : Semiconj fbc gb gc
x : α
⊢ (fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)

Tactic:
by
  simp only [comp_apply, hab.eq, hbc.eq]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
⊢ g ∘ f^[0] = g

Tactic:
by rw [iterate_zero, comp_id]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
⊢ Option.elim' b f a = a.elim b f

Tactic:
by
  cases a <;> rfl

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

Goal state before:
pp: α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : β → Option γ
H : ∀ (a : α), x = some a → p a
⊢ pmap f x H >>= g = x.pbind fun a h ↦ g (f a ⋯)

Tactic:
grind [cases Option, pmap]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
this : A_lt = B_lt
⊢ { le := le✝, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
    { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }

Tactic:
cases this

Goal state after:
case refl
α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ { le := le✝, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
    { le := le✝, lt := A_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
simp_rw [Pi.lt_def]
      rintro ⟨hab, i, hi⟩
      obtain ⟨c, ha, hb⟩ := exists_between hi
      exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩

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

Goal state before:
pp: k : ℕ
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
obtain rfl | hk : k = 0 ∨ k > 0 := k.eq_zero_or_pos

Goal state after:
case inl
⊢ 2 * 0 ^ 2 + 1 ≤ 2 ^ (2 * 0)

case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n m : ℕ
⊢ m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

Tactic:
rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.natCast_mul, Int.ofNat_two]

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| ⋯.by_cases (fun h ↦ le_succ_of_le h (leRec refl le_succ_of_le h)) fun h ↦
    Eq.ndrec (motive := fun {n} ↦
      {motive : (m : ℕ) → n ≤ m → Sort u_1} →
        motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → (H : n ≤ m + 1) → motive (m + 1) H)
      (fun {motive} refl le_succ_of_le H ↦ refl) ⋯ refl le_succ_of_le h2

Tactic:
Or.by_cases,

Goal state after:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| if hp : n ≤ m then le_succ_of_le hp (leRec refl le_succ_of_le hp)
  else
    Eq.ndrec (motive := fun {n} ↦
      {motive : (m : ℕ) → n ≤ m → Sort u_1} →
        motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → (H : n ≤ m + 1) → motive (m + 1) H)
      (fun {motive} refl le_succ_of_le H ↦ refl) ⋯ refl le_succ_of_le h2
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case self
a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
hP : P n
h : (k : ℕ) → k < n → n ≤ k → P (k + 1) → P k
⊢ P n

Tactic:
exact hP

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

Goal state before:
pp: case a.inr
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h✝ : a + 1 < b + 1
h : a + 1 < b
⊢ P (a + 1) b

Tactic:
apply diag_induction P ha hb hd (a + 1) b h

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a

pp: case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
· exact Iff.rfl

Goal state after:
case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a
Module: Mathlib.Order.Compare

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
· exact Iff.rfl

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.eq a b := hab

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a = b
hab : eq.Compares a b
⊢ o.Compares a b
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
constructor
  · intro h i x hf hg
    exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1
  · intro h x hf hg i
    apply h i (hf i) (hg i)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b → f a = f b

Tactic:
by
    rintro rfl
    rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ (f s).Nonempty ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]

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

Goal state before:
pp: 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.17
β : Type ?u.16
inst✝ : IsEmpty β
x : β
⊢ inl (Sum.elim id (fun a ↦ isEmptyElim a) (inr x)) = inr x

Tactic:
exact isEmptyElim x

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b

Tactic:
simp [symmDiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e'_3
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a = a ∆ ⊥

Tactic:
rw [symmDiff_bot]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e'_4
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b = b ∆ ⊥

Tactic:
rw [symmDiff_bot]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ ⊤ = ￢a

Tactic:
simp [symmDiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ∆ a = ￢a

Tactic:
simp [symmDiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = a ↔ a ∆ b = a ∆ ⊥

Tactic:
rw [symmDiff_bot]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ

Tactic:
rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
⊢ Disjoint (f '' s) (f '' sᶜ)

Tactic:
simp [disjoint_iff_inf_le, ← image_inter H]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f

Tactic:
rw [hf.range_eq]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a) ↔ ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
x✝ : a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
i : ι
h₁ : a ∈ univ.pi t
h₂ : ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
x : α i
hx : x ∈ t i
⊢ x = a i
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ f y = f z

Tactic:
← hz

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
z : α
hy : f y = f z
zt : z ∈ t
hz : f z = x
⊢ f y = f z
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
by rw [map_mul, map_inv]

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

Goal state before:
pp: a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d

Tactic:
Int.mul_assoc,

Goal state after:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * (k * d)
⊢ a = k * d
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ f val * f inv = 1

Tactic:
simp [← map_mul, val_inv]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ x✝ * 1 = x✝

Tactic:
by ext <;> exact mul_one _

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

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ ↑x✝¹.succ).1 = (x✝ ^ ↑x✝¹ * x✝).1

Tactic:
exact DivInvMonoid.zpow_succ' ..

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

Goal state before:
pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ ↑x✝¹.succ).2 = (x✝ ^ ↑x✝¹ * x✝).2

Tactic:
exact DivInvMonoid.zpow_succ' ..

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (g : α → β) (x : e ⊕ α), pure g <*> x = g <$> x

Tactic:
by
    intros
    rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : α) (f : α → e ⊕ β), pure x >>= f = f x

Tactic:
by
    intros
    rfl

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ y = z

Tactic:
← mul_inv_cancel_right₀ hx y,

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ y * x * x⁻¹ = z
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ single i 1 j • x = single i x j

Tactic:
single_apply,

Goal state after:
M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ (if j = i then 1 else 0) • x = single i x j
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a / b)

Tactic:
aesop (add simp div_eq_mul_inv)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
n : ℕ
inst✝ : n.AtLeastTwo
a : α
⊢ OfNat.ofNat n • a = OfNat.ofNat n * a

Tactic:
by
  simp [nsmul_eq_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1

Tactic:
rw [inv_eq_iff_mul_eq_one]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * k + 1)

Tactic:
hk

Goal state after:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -(2 * k + 1) = -(2 * k + 1)
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
β : Sort v
x✝¹ x✝ : α ≃ β
h : x✝¹.toEmbedding = x✝.toEmbedding
⊢ x✝¹ = x✝

Tactic:
by rwa [DFunLike.ext'_iff] at h ⊢

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
hb : b < 0
h : a < 1
⊢ b < a * b

Tactic:
by
  simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
hb : b < 0
h : 1 < a
⊢ a * b < b

Tactic:
by
  simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 2 * a * b + 2 * a * b ≤ a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
gcongr; exact two_mul_le_add_sq _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r ↪r s
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s ({ toFun := toFun✝, inj' := inj'✝ } a) ({ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h : (fun x ↦ x.toFun) { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ } = (fun x ↦ x.toFun) g
⊢ { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ } = g

Tactic:
rcases g with ⟨⟨⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
map_rel_iff'✝¹ :
  ∀ {a b : α}, s ({ toFun := toFun✝¹, inj' := inj'✝¹ } a) ({ toFun := toFun✝¹, inj' := inj'✝¹ } b) ↔ r a b
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s ({ toFun := toFun✝, inj' := inj'✝ } a) ({ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h :
  (fun x ↦ x.toFun) { toFun := toFun✝¹, inj' := inj'✝¹, map_rel_iff' := map_rel_iff'✝¹ } =
    (fun x ↦ x.toFun) { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ }
⊢ { toFun := toFun✝¹, inj' := inj'✝¹, map_rel_iff' := map_rel_iff'✝¹ } =
    { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ }
Module: Mathlib.Algebra.Order.Group.Lattice

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

Tactic:
rw [mul_comm, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ |a⁻¹|ₘ = |a|ₘ

Tactic:
by simp [mabs, sup_comm]

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

Goal state before:
pp: m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0

Tactic:
by_contra h
  have := Int.natAbs_le_of_dvd_ne_zero h1 h
  rw [Int.abs_eq_natAbs] at h2
  lia

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 : ℕ
⊢ 1 < ↑n ↔ 1 < n

Tactic:
rw [← cast_one, cast_lt]

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

Goal state before:
pp: α β γ : Type u
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = f <$> a <*> b

Tactic:
by
  cases a <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
b : β
⊢ map₂ f a ↑b = map (fun x ↦ f x b) a

Tactic:
by
  cases a <;> rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ exp x = 1 ↔ x = 0

Tactic:
← exp_zero,

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ exp x = exp 0 ↔ x = 0
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
by cases a <;> cases b <;> simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

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✝ : AddLeftReflectLE α
h : c ≤ b
⊢ a - (b - c) = a + c - b

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le h
  rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
⊢ ↑|a| = |↑a|

Tactic:
simp [abs_eq_max_neg]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case some
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
y : α
⊢ (∀ (a : α), Option.some y ≤ ↑a → x ≤ ↑a) ↔ x ≤ Option.some y

Tactic:
· exact ⟨fun h ↦ h _ le_rfl, fun hmn a ham ↦ hmn.trans ham⟩

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), y ≤ ↑a → x ≤ ↑a) ↔ x ≤ y

Tactic:
by
  obtain _ | y := y
  · simp [WithBot.none_eq_bot, eq_bot_iff_forall_le]
  · exact ⟨fun h ↦ h _ le_rfl, fun hmn a ham ↦ hmn.trans ham⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z - 1 < ⌈a⌉ ↔ ↑z - 1 < a

Tactic:
lt_ceil

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ↑(z - 1) < a ↔ ↑z - 1 < a
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
⊢ x ≤ exp a

Tactic:
obtain rfl | hx := eq_or_ne x 0 <;> simp [← log_le_iff_le_exp, *]

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 : ℕ
⊢ a ≤ ⌊↑n⌋₊ ↔ a ≤ n

Tactic:
rw [le_floor_iff, Nat.cast_le]

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ 0 ≤ ↑n
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
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋₊

Tactic:
simp [floor_lt, ha]

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

Tactic:
lt_ceil

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d < a ↔ d < ⌈a⌉₊

Tactic:
lt_ceil

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d < a ↔ ↑d < a