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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Total r
a b : α
⊢ Decidable.decide (r a b) = true ∨ Decidable.decide (r b a) = true

Tactic:
simpa using total a b

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

Goal state before:
pp: ⊢ @npowRecAuto = @npowBinRecAuto

Tactic:
funext M _ _ k m
  rw [npowBinRecAuto, npowRecAuto, npowBinRec]
  match k with
  | 0 => rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
  | k + 1 => rw [npowBinRec.go_spec, npowRec_eq]

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

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = extend f₁₂ g (e' ∘ f₂₃) (f₁₂ c)

Tactic:
h₁₂.extend_apply

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case neg
γ : 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
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]
      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: case mp
α : 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

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Tactic:
· exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y

Tactic:
· by_cases h₁ : y.1 ≤ x.1
    · exact Or.inr ⟨h.1.1, LE.le.lt_of_not_ge h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
    · exact Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
Module: Mathlib.Order.Basic

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

Tactic:
by
  by_contra hne
  simp only [not_or, ← Ne.eq_def] at hne
  rcases hne.1.lt_or_gt with h₁ | h₁ <;>
  rcases hne.2.1.lt_or_gt with h₂ | h₂ <;>
  rcases hne.2.2.lt_or_gt with h₃ | h₃
  exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]

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

Goal state before:
pp: n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
hmk : m ≤ k
⊢ leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk

Tactic:
induction hmk with

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)

Tactic:
rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn),
    decreasingInduction_trans (n := m + 1) (Nat.le_succ m),
    decreasingInduction_succ']

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
eq_bot_iff,

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ s ⊂ univ ↔ sᶜ.Nonempty

Tactic:
ssubset_def,

Goal state after:
α : Type u
s : Set α
⊢ s ⊆ univ ∧ ¬univ ⊆ s ↔ sᶜ.Nonempty
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:
sup_idem

Goal state after:
α✝ : 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 ⊔ b = a ⊔ b
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 ⊔ (b ⊔ b) = a ⊔ b

Tactic:
sup_idem

Goal state after:
α✝ : 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 ⊔ b = a ⊔ b
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ sᶜ ⊂ univ ↔ s.Nonempty

Tactic:
ssubset_def,

Goal state after:
α : Type u
s : Set α
⊢ sᶜ ⊆ univ ∧ ¬univ ⊆ sᶜ ↔ s.Nonempty
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ a ⊔ (b ⊔ c)

Tactic:
sup_idem

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ (b ⊔ c)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ b ⊔ (c ⊔ c)

Tactic:
sup_idem

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ b ⊔ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b ≤ a ⊓ b ↔ a = b

Tactic:
sup_le_inf

Goal state after:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a = b ↔ a = b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
by rw [le_himp_iff, inf_top_eq]

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ Disjoint a b

Tactic:
by
  rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ z ⊔ (x ⊔ x) ≤ z ⊔ x

Tactic:
sup_idem

Goal state after:
α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ z ⊔ x ≤ z ⊔ x
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).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩

Goal state after:
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₁
⊢ s ⊆ s₁

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₁

case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Injective (restrict f s t h) ↔ InjOn f s

Tactic:
by
  rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map f h) = Subtype.val ⁻¹' f '' {x | p x}

Tactic:
by
  ext ⟨x, hx⟩
  simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map]
  simp only [Subtype.mk.injEq, exists_prop, mem_ofPred_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s.Nontrivial
hf : Surjective f
⊢ (f ⁻¹' s).Nontrivial

Tactic:
rcases hs with ⟨fx, hx, fy, hy, hxy⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
⊢ (f ⁻¹' s).Nontrivial
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
⊢ eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Tactic:
by
  classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : ↑s → β
hf : Injective f
⊢ ∃ f, InjOn f s

Tactic:
by
    lift f to α → β using trivial
    exact ⟨f, injOn_iff_injective.2 hf⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂

Tactic:
ssubset_def,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊆ f '' s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
b : β
hb : b ∈ t
⊢ p b

Tactic:
obtain ⟨a, ha, rfl⟩ := hf.surjOn hb

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
⊢ ∃ a, a ∈ s ∧ p (f a)

Tactic:
obtain ⟨a, ha, rfl⟩ := hf.surjOn hb

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ a, a ∈ s ∧ p (f a)
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✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ f.comp 1 = 1

Tactic:
by
  ext
  simp only [map_one, coe_comp, Function.comp_apply, one_apply]

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
⊢ Int.inductionOn' (z - 1) b zero succ pred = pred z hz (Int.inductionOn' z b zero succ pred)

Tactic:
unfold Int.inductionOn'
  conv => lhs; unfold inductionOn'.neg
  by_cases z = b
  · rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = 0 by lia]
    grind [inductionOn'.pos]
  rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = -[(b - z - 1).toNat+1] by lia]
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁

case refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'

case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)

case refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
⊢ SurjOn (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Tactic:
rintro x hx

Goal state after:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
⊢ x ∈ (fun x ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
h : a = b⁻¹
⊢ b⁻¹ * b = 1

Tactic:
inv_mul_cancel

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
h : a = b⁻¹
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ ↑b⁻¹ * a = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b

Tactic:
rw [mul_comm, mul_comm _ c, mul_inv_eq_mul_inv_iff]

Goal state after:
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:
by
    rw [zero, one]
    exact zero_ne_one

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

Goal state before:
pp: G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a * (b * b⁻¹) = a

Tactic:
mul_inv_cancel₀ hb,

Goal state after:
G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a * 1 = a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
· rw [zero_pow h]

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 : x * y = x * z
⊢ y = z

Tactic:
rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]

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

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

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

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

Goal state before:
pp: case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ IsSquare (-↑i✝ - 1).sign ↔ 0 ≤ -↑i✝ - 1

Tactic:
| pred =>

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

Tactic:
simp_rw [isLeftCancelMulZero_iff, isRightCancelMulZero_iff, isCancelMulZero_iff_forall_isRegular,
    isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul,
    isRegular_iff_eq_zero_of_mul]

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α

Tactic:
isDomain_iff_cancelMulZero_and_nontrivial

Goal state after:
α : Type u_3
inst✝ : Ring α
⊢ IsCancelMulZero α ∧ Nontrivial α ↔ IsCancelMulZero α ∧ Nontrivial α
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ f n = (zpowersHom α).symm f ^ toAdd n

Tactic:
← zpowersHom_apply,

Goal state after:
α : Type u_3
inst✝ : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ f n = ((zpowersHom α) ((zpowersHom α).symm f)) n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
· exact (h _ bc).le

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
⊢ IsUnit 2 ↔ ∀ (a : α), Even a

Tactic:
by
  refine ⟨Even.of_isUnit_two, fun h => ?_⟩
  obtain ⟨a, ha⟩ := h 1
  rw [← two_mul, eq_comm] at ha
  exact ⟨⟨2, a, ha, .trans (Commute.ofNat_right _ _).eq ha⟩, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a⁻¹ * a ≤ b * a ↔ 1 ≤ b * a

Tactic:
inv_mul_cancel

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 ≤ b * a ↔ 1 ≤ b * a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a * b ≤ b⁻¹ * b ↔ a * b ≤ 1

Tactic:
inv_mul_cancel

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a * b ≤ 1 ↔ a * b ≤ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel

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

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

Tactic:
inv_mul_cancel

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a * b < 1 ↔ a * b < 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) a b) ((fun x y ↦ y * ↑x) a c)
ha : 0 < ↑a
⊢ b < c

Tactic:
exact @ContravariantClass.elim α>0 α (fun x y => y * x) (· < ·) _ ⟨_, ha⟩ _ _ 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:
rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]

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

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

Tactic:
by rwa [← nsmul_one]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℕ
hn : x < n • 1
⊢ x < ↑n

Tactic:
by rwa [← nsmul_one]

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 / b ⊔ b / a ⊔ (1 ⊔ 1) = |b / a|ₘ

Tactic:
sup_idem

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

Goal state before:
pp: a b : ℤ
H : b ≠ 0
⊢ a % b < |b|

Tactic:
rw [← emod_abs]

Goal state after:
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
apply le_of_mul_le_of_one_le_left _ (one_le_mabs _); rw [mabs_div_sup_mul_mabs_div_inf]

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
simp [← not_even_iff_odd, not_or, parity_simps]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ a / min a b = |a / b|ₘ

Tactic:
min_eq_right ba,

Goal state after:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ a / b = |a / b|ₘ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ (a ^ m.gcd n) ^ (m / m.gcd n) = 1

Tactic:
hmn,

Goal state after:
case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 ^ (m / m.gcd n) = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ (a ^ m.gcd n) ^ (n / m.gcd n) = 1

Tactic:
hmn,

Goal state after:
case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 ^ (n / m.gcd n) = 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b

Tactic:
by
  refine fun x y xy => ab (?_ : x * (b * a) = y * (b * a))
  rw [← mul_assoc, ← mul_assoc]
  exact congr_arg (· * a) xy

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - ⊤ = ⊤

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ b⁻¹ * a < c

Tactic:
rw [mul_comm] at *

Goal state after:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < c * b
⊢ a * b⁻¹ < c
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
x y : WithBot α
⊢ x ≤ y → y ≤ x → x = y

Tactic:
cases x <;> cases y <;> simp [le_def]; simpa using le_antisymm

Goal state after: