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

Goal state before:
pp: case succ.zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 + 1 ≠ 0
⊢ npowRec (m + (0 + 1)) a = npowRec m a * npowRec (0 + 1) a

Tactic:
simp only [npowRec, ha]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
⊢ flip (r ∘r p) = flip p ∘r flip r

Tactic:
funext c a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
use cases_head

Goal state after:
case mpr
α : Type u_1
r : α → α → Prop
a b : α
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
a b b✝ : α
hc : r a b✝
⊢ r a b✝

Tactic:
exact hc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1.tail
α : Type u_1
r : α → α → Prop
a b b✝ : α
hac : ReflTransGen r a b✝
hcb : r b✝ b
⊢ b = a ∨ TransGen r a b

Tactic:
exact Or.inr (TransGen.tail' hac hcb)

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
eqvGen_symmGen

Goal state after:
α : Type u_1
r : α → α → Prop
⊢ EqvGen r = EqvGen r
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.Associative gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))

Tactic:
simp only [h.eq, Std.Associative.assoc (op := gb)]

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

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝ : ∃ b, q b
a : β
h : q a
⊢ q (e (e.symm a))

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
⊢ ∃ a, f a = c

Tactic:
obtain ⟨⟨a, b⟩, h⟩ := h (c, default)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ a, f a = c
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by
  obtain h | h | h := lt_trichotomy a b <;> simp [le_of_lt, not_le_of_gt, h, min_def]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ ¬f a = f b

Tactic:
rename_i h

Goal state after:
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : ¬a < b
h : ¬a = b
⊢ ¬f a = f b
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m✝ n✝ k : ℕ
p : ℕ → Prop
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
m : ℕ
mn : m ≤ n
⊢ motive m mn

Tactic:
by
  induction mn using leRec with
  | refl => exact self
  | @le_succ_of_le k _ ih =>
    apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b

Tactic:
rw [← sup_assoc, sup_idem]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ {a} ∩ s = ∅ ↔ ¬a ∈ s

Tactic:
singleton_inter_eq_empty

Goal state after:
α : Type u_1
s : Set α
a : α
⊢ ¬a ∈ s ↔ ¬a ∈ s
Module: Mathlib.Order.Lattice

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Lattice α
a c : α
h : a ⊓ a = c ∧ a ⊔ a = c
⊢ a = c ∧ a = c

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f x ⊔ f y = f y

Tactic:
← h _ hx _ hy,

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f (x ⊔ y) = f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f x ⊔ f y = f x

Tactic:
← h _ hx _ hy,

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f (x ⊓ y) = f x
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
⊢ DistribLattice α

Tactic:
let lattice := e.lattice
  apply e.injective.distribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ≤ ⊤ ⇨ a ↔ b ≤ a

Tactic:
rw [le_himp_iff, inf_top_eq]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : a ≤ b
⊢ ⊥ ≤ c ↔ a ≤ max b c

Tactic:
exact iff_of_true bot_le (le_sup_of_le_left h)

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

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_none _ h2] at h1
        simp at h1

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
bot_sdiff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ⊔ ⊥ = a
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
⊢ f x ∈ g ⁻¹' s ↔ x ∈ s

Tactic:
Set.mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
⊢ g (f x) ∈ s ↔ x ∈ s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ range (inclusion h) = {x | ↑x ∈ s}

Tactic:
by
  ext ⟨x, hx⟩
  simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s

Tactic:
by
  rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]

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

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

Tactic:
by
  rw [← image_univ]
  simp [-image_univ, coe_image]

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
⊢ update f i x j ∈ t j

Tactic:
obtain rfl | h := eq_or_ne j i
    · simpa
    · rw [update_of_ne h]
      exact hf j hj h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Subsingleton β
inst✝ : Nonempty β
⊢ SurjOn f s univ ↔ s.Nonempty

Tactic:
cases nonempty_unique β; simp [univ_unique, Subsingleton.elim (f _) default, Set.Nonempty]

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h✝ : t₂.Nonempty
x✝ : β₁
h : x✝ ∈ t₁
⊢ x✝ ∈ Prod.fst '' t₁ ×ˢ t₂

Tactic:
simpa [h]

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h✝ : t₁.Nonempty
x✝ : β₂
h : x✝ ∈ t₂
⊢ x✝ ∈ Prod.snd '' t₁ ×ˢ t₂

Tactic:
simpa [h]

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ t₁ = ∅ ∨ t₂.Nonempty → SurjOn Prod.fst (t₁ ×ˢ t₂) t₁

Tactic:
simp +contextual [or_imp, prod_surjOn_fst]

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

Goal state before:
pp: case mp
M : Type u_4
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1

Tactic:
simpa using h

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

Goal state before:
pp: case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
simp only [one_div, inv_zpow]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]

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

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

Tactic:
rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, 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✝).1 = (x✝¹ * x✝⁻¹).1

Tactic:
exact div_eq_mul_inv ..

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✝).2 = (x✝¹ * x✝⁻¹).2

Tactic:
exact div_eq_mul_inv ..

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
x : G₀
hx : f x ≠ 0
⊢ f (x * x⁻¹) = 1

Tactic:
mul_inv_cancel₀ (mt (congr_arg f) fun h ↦ hx (h.trans zero)),

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
x : G₀
hx : f x ≠ 0
⊢ f 1 = 1
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
y : B
x : A
⊢ c • (f x + y) = c • f x + c • y

Tactic:
rcases hf y with ⟨y, rfl⟩

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
x y : A
⊢ c • (f x + f y) = c • f x + c • f y
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

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

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

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

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

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

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → IsLeftRegular a, ∀ {a : R}, a ≠ 0 → IsRightRegular a, IsCancelMulZero R].TFAE

Tactic:
isCancelMulZero_iff_forall_isRegular,

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → IsLeftRegular a, ∀ {a : R}, a ≠ 0 → IsRightRegular a,
      ∀ {a : R}, a ≠ 0 → IsRegular a].TFAE
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ʳ = a⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · simp
  · exact Ring.inverse_unit (Units.mk0 a ha)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + -(2 * a * b) + b ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
← sub_eq_add_neg

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 - 2 * a * b + b ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + b ^ 2 + -(2 * a * b) = a ^ 2 + b ^ 2 - 2 * a * b

Tactic:
← sub_eq_add_neg

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + b ^ 2 - 2 * a * b = a ^ 2 + b ^ 2 - 2 * a * b
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑↑n) x

Tactic:
by simpa using n.cast_commute x

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

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ ¬Even n

Tactic:
simpa using h

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

Goal state before:
pp: case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
· exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_lt_of_le h.1.1 h.2.2.le

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

pp: case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
· exact mul_lt_mul_of_lt_of_le ha' hb

Goal state after:
case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : a ≤ 1
⊢ a * b ≤ b

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

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a * b

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

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ fst.prod snd = id

Tactic:
ext ⟨x, y⟩ : 2
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
rw [mabs_of_le_one ha, mabs_of_le_one (hab.trans ha)]; exact inv_le_inv_iff.mpr hab

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

Goal state before:
pp: case inl
n r : ℕ
hkn : n.Coprime 1
hk : 1 ≠ 0
⊢ ∃ m, m < 1 ∧ n * m % 1 = r % 1

pp: case inr
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
⊢ ∃ m, m < k ∧ n * m % k = r % k

Tactic:
· simp [mod_one]

Goal state after:
case inr
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
⊢ ∃ m, m < k ∧ n * m % k = r % k
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : Nonempty α
ha : ⊥ ≠ ⊥
⊢ ⊥.unbotA = ⊥.unbot ha

Tactic:
| bot =>

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

Goal state before:
pp: case pos
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
rw [findGreatest_eq hk]
      constructor
      · rintro rfl
        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by lia⟩
      · rintro ⟨hle, h0, hm⟩
        rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
        exacts [(hm hlt (le_refl _) hk).elim, rfl]

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

Goal state before:
pp: m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
⊢ P (findGreatest P n)

Tactic:
by
  by_cases h : Nat.findGreatest P n = 0
  · cases m
    · rwa [h]
    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim
  · exact (findGreatest_eq_iff.1 rfl).2.1 h

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌊a⌋ ≤ z ↔ a < ↑z + 1

Tactic:
rw [← lt_add_one_iff, floor_lt]

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ a < ↑(z + 1) ↔ a < ↑z + 1
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
⊢ ⌈a + ↑1⌉₊ = ⌈a⌉₊ + 1

Tactic:
ceil_add_natCast ha 1

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌈a⌉₊ + 1 = ⌈a⌉₊ + 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.bot
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
hc : ↑a < ⊥ ∧ ⊥ < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
| bot =>

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ a / -a = -1

Tactic:
by rw [div_neg_eq_neg_div, div_self h]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsLeast (f '' s) (f a) ↔ IsLeast s a

Tactic:
simp [IsLeast, hf.injective.eq_iff, hf.mem_lowerBounds_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2

Tactic:
refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
  · suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
    exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
  · suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
    exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
  · exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
  · exact fun q hq =>
      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t

Tactic:
(_ : t \ s ∪ s ∩ t = t)

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑s ⊕ ↑t ≃ ↑s ⊕ ↑t

α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ t \ s ∪ s ∩ t = t
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Iic a ⊂ Iic b
⊢ a < b

Tactic:
obtain ⟨ab, c, cb, ac⟩ := ssubset_iff_exists.mp h
    exact lt_of_le_not_ge (Iic_subset_Iic.mp ab) (fun h' ↦ ac (cb.trans h'))

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
by_cases hb : b ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}