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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n % 2 = b.toNat

Tactic:
cases b <;> simp [bit_val]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
⊢ ∃ x, f x ≠ y

Tactic:
rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
  by_cases h : f x₂ = y
  · exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
  · exact ⟨x₂, h⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x

Tactic:
by_cases hx : x = y

Goal state after:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_3
⊢ Subsingleton α ∨ Nontrivial α

Tactic:
rw [← not_nontrivial_iff_subsingleton, or_comm]
  exact Classical.em _

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)

Tactic:
Xor,

Goal state after:
a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∨ b) ∧ ¬(a ∧ b)
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ False

Tactic:
or_false

Goal state after:
a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
⊢ False

Tactic:
let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩

Goal state after:
case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
⊢ False
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ ¬∃ a, (f₂₃ ∘ f₁₂) a = f₂₃ b

Tactic:
exact fun h ↦ h₂ (Exists.casesOn h fun c hc ↦ Exists.intro c (h₂₃ hc))

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
by
  induction h with
  | single h => exact single h
  | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)

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

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty α
⊢ BiTotal R ↔ IsEmpty β

Tactic:
by
  simp only [BiTotal, leftTotal_empty, rightTotal_iff_isEmpty_right, true_and]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by
  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.Max

Goal state before:
pp: α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoBotOrder α
a : α
⊢ ∃ b, b < a

Tactic:
by simpa [not_le] using exists_not_ge a

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

Goal state before:
pp: ⊢ bne = xor

Tactic:
by constructor

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
rw [← not_iff_not, not_lt, Int.mul_nonneg_iff]
  lia

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

Goal state before:
pp: case neg
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq

Goal state after:
case neg
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Module: Mathlib.Order.Lattice

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

Tactic:
by
  let le := e.le
  let lt := e.lt
  apply Function.Injective.preorder e <;> intros <;> rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ c ≤ a \ b ⊔ b \ c

Tactic:
by
  rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
  exact sdiff_sdiff_le.trans le_sup_sdiff

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint (a ⊓ b) (a ⊓ b)ᶜ

Tactic:
exact disjoint_compl_right

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

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

Tactic:
simp [removeNoneAux, Option.not_isSome_iff_eq_none.mpr h]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x

Tactic:
rw [← disjoint_iff]
  exact disjoint_sdiff_iff_le hz hx

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

Tactic:
by_cases h : p a <;> simp [Perm.subtypeCongr, h]

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
⊢ s ⊆ s₁

Tactic:
rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁

Tactic:
have := image_mono (f := Prod.snd) H

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ ∃ a_1, restrict f s t h a_1 = ⟨f a, hb⟩

Tactic:
exact ⟨⟨a, ha⟩, rfl⟩

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ False ↔ s = s₁ ∧ t = t₁

Tactic:
or_false

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ (s = ∅ ∨ False) ∧ (s₁ = ∅ ∨ False) → s = s₁

Tactic:
or_false

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = ∅ ∧ s₁ = ∅ → s = s₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s

Tactic:
by
  rw [← preimage_sumElim, Sum.elim_inl_inr, preimage_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ MapsTo f s ∅ ↔ s = ∅

Tactic:
simp [mapsTo_iff_image_subset, subset_empty_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SurjOn id s s

Tactic:
simp [SurjOn]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
g : N →* P
f₁ f₂ : M →* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
← MonoidHom.comp_apply,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
g : N →* P
f₁ f₂ : M →* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₁) x = g (f₂ x)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ a < a.succ

Tactic:
by unfold succ; lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (x✝ ^ ↑x✝¹.succ) = unop (x✝ ^ ↑x✝¹ * x✝)

Tactic:
HPow.hPow,

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (Pow.pow x✝ ↑x✝¹.succ) = unop (Pow.pow x✝ ↑x✝¹ * x✝)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = 1

Tactic:
rw [← zpow, zpow_zero, ← one]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a c = f a b * f b c

Tactic:
rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a b * (f b a * f a c) = f a b * f b c
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬f 0 = f 1

Tactic:
zero,

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = f 1
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
β : Type u_8
⊢ Function.Injective ⇑(sumCongrHom α β)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Goal state after:
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑(subtypeCongrHom p)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
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₀' ℤ
f : G₀' → G₀
hf : Injective 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
⊢ (f 0)⁻¹ = f 0

Tactic:
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₀' ℤ
f : G₀' → G₀
hf : Injective 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
⊢ 0⁻¹ = 0
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

Tactic:
rw [← succ_mul]

Goal state after:
n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt
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:
by aesop (add simp div_eq_mul_inv)

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

Goal state before:
pp: l : List Prop
⊢ (map Not l).TFAE ↔ l.TFAE

Tactic:
classical
  simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Decidable.not_iff_not]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + -n) = a ^ m / a ^ n

Tactic:
zpow_add₀ ha,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ m * a ^ (-n) = a ^ m / a ^ n
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, by rw [mul_add, ← two_mul, add_assoc]⟩

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

Goal state before:
pp: β : Sort u_1
b : β
⊢ Injective fun x ↦ b

Tactic:
by
    rintro ⟨⟩ ⟨⟩ _
    rfl

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
⊢ a * c ≤ b

Tactic:
rwa [le_mul_inv_iff₀ hc] at h

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
⊢ ∀ (a : α), a = g (f a)

Tactic:
by
    intro
    rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]

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

Goal state before:
pp: case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1

Tactic:
rw [mabs_of_one_lt ab, mul_left_inj] at h
    rw [eq_one_of_inv_eq' h.symm] at ha
    cases ha.false

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a / a ⊔ a / b ⊔ (b / a ⊔ b / b) = |b / a|ₘ

Tactic:
div_self',

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ 1 ⊔ a / b ⊔ (b / a ⊔ 1) = |b / a|ₘ
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a / a|ₘ ≤ 1

Tactic:
div_self',

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |1|ₘ ≤ 1
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ Injective ⇑(map' f) ↔ Injective ⇑f

Tactic:
by
  simp [Injective, WithZero.forall]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

Tactic:
simp [lt_top_iff_ne_top]

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

Tactic:
grw [add_tsub_le_left]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ a - c < b - c ↔ a < b

Tactic:
hc.lt_tsub_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ c + (a - c) < b ↔ a < b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b + b = max a b

Tactic:
rcases le_total a b with h | h
  · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
  · rw [max_eq_left h, tsub_add_cancel_of_le h]

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

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ a + b = a + c → b = c

Tactic:
simpa using @ha _ _

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

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ b + a = c + a → b = c

Tactic:
simpa using @ha _ _

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]

Tactic:
by
    have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
    simpa [(negSucc_lt_zero n).not_ge, ← sub_eq_add_neg, le_neg] using this.not_ge

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← sub_nonneg, ← cast_sub, cast_nonneg_iff, sub_nonneg]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : WithBot α
b : α
h : a ≠ ⊥
⊢ a.unbot h = b ↔ a = ↑b

Tactic:
by
  induction a
  · simpa using h rfl
  · simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a : (Additive α)ᵒᵈ
⊢ ⊥ * Additive.toMul (OrderDual.ofDual a) = ⊥

Tactic:
simp [bot_eq_zero (α := α)]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
⊢ b < d

Tactic:
by
  have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
  rw [← inv_le_inv₀ ha.pos hc] at hh
  simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne']
    using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh h zero_le (inv_pos.2 hc)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedAddCommMonoidWithTop α
a : α
ha : 0 < Multiplicative.ofAdd (OrderDual.toDual a)
b c : α
hbc : c < b
⊢ a ≠ ⊤

Tactic:
by simpa using! ha.ne'

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ ⌊a⌋ < 0 ↔ a < 0

Tactic:
floor_lt,

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ a < ↑0 ↔ a < 0
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
⊢ ∃ z, z ≠ 0 ∧ z < x ∧ z < y

Tactic:
obtain ⟨z, hnz, hlt⟩ := exists_ne_zero_and_lt hnz'

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ ∃ z, z ≠ 0 ∧ z < x ∧ z < y
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b✝ : α
x✝¹ x✝ : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self✝ : c * a = 1
hac : a * c = 1
⊢ { invOf := b, invOf_mul_self := hba, mul_invOf_self := hab } =
    { invOf := c, invOf_mul_self := invOf_mul_self✝, mul_invOf_self := hac }

Tactic:
congr
    exact left_inv_eq_right_inv hba hac

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(-x.mulRight ↑y) = ↑x * ↑(-y)

Tactic:
apply AddUnits.neg_eq_of_add_eq_zero_left

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑x * ↑(-y) + ↑(x.mulRight ↑y) = 0
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
G : Type u_4
inst✝ : LeftCancelSemigroup G
g : G
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | ⟨val, h⟩ => Exists.choose h)
    fun a ↦ ⟨g * a, ⋯⟩

Tactic:
rintro ⟨_, ⟨_, rfl⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
G : Type u_4
inst✝ : LeftCancelSemigroup G
g w✝ : G
⊢ (fun a ↦ ⟨g * a, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨val, h⟩ => Exists.choose h)
        ⟨g * w✝, ⋯⟩) =
    ⟨g * w✝, ⋯⟩
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
obtain rfl | ha := eq_or_ne a 0; · simp
  rw [← mul_eq_one_iff_inv_eq₀ ha, ← pow_two, sq_eq_one_iff]
  tauto

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

Goal state before:
pp: n : ℕ
⊢ IsUnit ↑n ↔ IsUnit n

Tactic:
by simp [isUnit_iff_natAbs_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (a : α), a ∈ s → (fun b ↦ f a b) '' t ⊆ u

Tactic:
by
  simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ uncurry f '' s ×ˢ (t ∩ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'

Tactic:
prod_inter,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ uncurry f '' (s ×ˢ t ∩ s ×ˢ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
⊢ image2 f s {b} = s

Tactic:
by
  rw [image2_singleton_right, funext h, image_id']

Goal state after: