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

Goal state before:
pp: n : Nat
x✝ : n % 2 = 0 ∨ n % 2 = 1
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
cases mod_two_eq_zero_or_one n with

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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
reg : IsRightRegular a
⊢ Commute (b * a) a ↔ Commute a b

Tactic:
simp [commute_iff_eq, ← mul_assoc, reg.eq_iff, eq_comm]

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

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec k m = npowBinRec.go k 1 m

Tactic:
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.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ b

Tactic:
apply h₂.elim

Goal state after:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ ∀ (x : α), (∃ h, q x h) → (∀ (y : α), (∃ h, q y h) → y = x) → b
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 / x

Tactic:
rw [div_eq_mul_inv, one_mul]

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

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

Tactic:
← inv_eq_of_mul_eq_one_right h,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : a * b = 1
⊢ a⁻¹⁻¹ = a
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ x' ≠ y'

Tactic:
refine fun H ↦ h ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ f x' = y

Tactic:
← hy',

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ f x' = f y'
Module: Mathlib.Logic.Relation

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

Tactic:
by rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hp : r ≤ p
a : α
⊢ ReflGen p a a

Tactic:
by rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ motive a ⋯

Tactic:
apply ih
  · exact head hbc _ refl
  · exact fun h1 h2 ↦ head h1 (h2.tail hbc)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ReflTransGen r a a

Tactic:
by rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c b✝ : α
hac : r a b✝
⊢ ReflTransGen r b✝ b✝

Tactic:
by rfl

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

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

Tactic:
rwa [iterate_succ, ← comp_assoc, iterate_invariant h m]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x ↦ f b) a (b :: l) = f^[(b :: l).length] a

Tactic:
rw [length_cons, foldl, iterate_succ_apply, H]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = g⁻¹ • b

Tactic:
by rw [← h, inv_smul_smul]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ max a b = if a < b then b else a

Tactic:
rw [max_comm, max_def, ← ite_not]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then b else a) = if a < b then b else a
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
simpa [hx, hy] using hfg hx hy h

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

Goal state before:
pp: β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)

Tactic:
rcases lt.dest hab with ⟨n, rfl⟩
  clear hab
  induction n with
  | zero => rw [Int.ofNat_one]; apply h
  | succ n ihn => rw [Int.natCast_succ, ← Int.add_assoc]; exact _root_.trans ihn (h _)

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n : ℕ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℕ
⊢ f a ≠ x

Tactic:
rintro rfl
  exact (hf.reflect_lt h1).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h2)

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
by
  rw [sup_comm, sup_comm a, sup_assoc]

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

Goal state before:
pp: p q : Prop
⊢ q ∈ {p}ᶜ ↔ q ∈ {¬p}

Tactic:
by simpa [@Iff.comm q] using not_iff

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
by
  simp only [sup_inf_left, sup_comm _ c]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : a ≤ b
⊢ p (max a b)

Tactic:
sup_eq_right.2 h

Goal state after:
α : Type u
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : a ≤ b
⊢ p b
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y

Tactic:
rintro rfl x
    exact (gc x y).symm

Goal state after:
Module: Mathlib.Order.Lattice

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

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

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
apply e.injective.distribLattice <;> intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_sdiff_eq_sup hab,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ⊔ c = c
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
x : (α ⊕ γ) ⊕ β ⊕ δ
⊢ (⇑(sumAssoc (α ⊕ γ) β δ) ∘
        Sum.map (⇑(sumAssoc α γ β).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
      ((⇑(sumAssoc (α ⊕ β) γ δ) ∘
          Sum.map (⇑(sumAssoc α β γ).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
        x) =
    x

Tactic:
by rcases x with ((a | c) | (b | d)) <;> simp

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

Goal state before:
pp: α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ Set.image (⇑(swap i j)) s ↔ a ∈ insert j s \ {i}

Tactic:
constructor
    · rintro ⟨a, ha, rfl⟩
      obtain rfl | ne := eq_or_ne a i
      · rw [swap_apply_left]; exact ⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩
      · rw [swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)]; exact ⟨.inr ha, ne⟩
    · rintro ⟨rfl | has, hai⟩
      · exact ⟨i, hi, swap_apply_left ..⟩
      · exact ⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c

Tactic:
exact sup_le_sup le_sup_right le_sup_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = Subtype.val ⁻¹' f ⁻¹' Subtype.val '' u

Tactic:
← image_val_preimage_restrictPreimage,

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = Subtype.val ⁻¹' Subtype.val '' t.restrictPreimage f ⁻¹' u
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp.h₁
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t

Tactic:
← preimage_subset_preimage_iff hs,

Goal state after:
case mp.h₁
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ f ⁻¹' s ⊆ f ⁻¹' t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: X : Type ?u.21
Y : Sort ?u.6
Z : Type ?u.22
f : X → Y
g : Z → X
inj : Injective g
⊢ f ∘ g = id ∘ f ∘ g

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
⊢ f '' s = range f ∩ g ⁻¹' s

Tactic:
rw [← image_preimage_eq_range_inter, hfg.preimage_preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ x = y

Tactic:
simpa using @h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa [imageFactorization])

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : ↑a * b = ↑a * c
⊢ b = c

Tactic:
by simpa only [inv_mul_cancel_left] using congr_arg (fun x : α => ↑(a⁻¹ : αˣ) * x) h

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

Goal state before:
pp: G : Type u_6
inst✝ : Group G
x : Gˣ
⊢ toUnits ↑x = x

Tactic:
by
  simp_rw [← MulEquiv.eq_symm_apply, toUnits_symm_apply]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
by rw [Hfa, zero]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
by rw [Hfa, zero]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
a : α
f : F
neZero : NeZero (f a)
h : a = 0
⊢ f a = 0

Tactic:
rw [h]; exact ZeroHomClass.map_zero f

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

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
hb : b ≠ 0
⊢ a * b = b ↔ a = 1

Tactic:
mul_eq_right₀ hb

Goal state after:
M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
hb : b ≠ 0
⊢ a = 1 ↔ a = 1
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
a : α
x : β
h : a • x = 0
⊢ x = 0

Tactic:
by rw [← inv_smul_smul a x, h, smul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + -[n+1]) = ↑↑m + ↑-[n+1]

Tactic:
Int.ofNat_add_negSucc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat m n.succ) = ↑↑m + ↑-[n+1]
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ a ^ 2 + (2 * a * b + b ^ 2) = a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
add_comm _ (b ^ 2),

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
⊢ a ^ 2 + (b ^ 2 + 2 * a * b) = a ^ 2 + b ^ 2 + 2 * a * b
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
⊢ { toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } = 1

Tactic:
by
    ext1 f
    exact one_comp f

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ -(x * x - b * x) = x * (b - x)

Tactic:
simp [mul_sub, mul_comm]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
c : G₀
hc : c ≠ 0
a b : G₀
⊢ a / c * c / b = a / b

Tactic:
div_mul_cancel₀ _ hc

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
c : G₀
hc : c ≠ 0
a b : G₀
⊢ a / b = a / b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a / c * c = b / d * c

Tactic:
div_mul_cancel₀ _ hc

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a = b / d * c
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ (a * if h0 : a = 0 then 0 else ↑⋯.unit⁻¹) = 1

Tactic:
dif_neg h0,

Goal state after:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ a * ↑⋯.unit⁻¹ = 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
⊢ Even (-2)

Tactic:
by simp only [even_neg, even_two]

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

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = f
hn : Even n
⊢ f = id

Tactic:
hf.iterate_even hn,

Goal state after:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : id = f
hn : Even n
⊢ f = id
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ f a

Tactic:
rwa [← zero, le]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ f a

Tactic:
rwa [← zero, le]

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

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

Tactic:
← mul_lt_mul_iff_left a

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a * b < a * (a⁻¹ * c) ↔ a * b < c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a / d ≤ b / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]
  exact mul_le_mul' hab hcd

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c

Tactic:
simpa using mul_le_mul_right bc a⁻¹

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : b * a ≤ c * a
⊢ b ≤ c

Tactic:
simpa using mul_le_mul_right bc a⁻¹

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg ha.le hb

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
← inv_le_inv₀ (inv_pos.2 hb) ha,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹
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
r : β → β → Prop
f : α ↪ β
⊢ ∀ {a b : α}, r (f a) (f b) ↔ (r on ⇑f) a b

Tactic:
by rfl

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

Goal state before:
pp: case inr.inl.inl
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 : a * b ≤ 1
⊢ b ≤ 1

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:
· refine (eq_one_of_inv_eq' ?_).le
    rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h

Goal state after:
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
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
az : a = 0
⊢ a.sign = a / |a|

Tactic:
by simp [az]

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

Goal state before:
pp: a : ℤ
az : a = 0
⊢ a.sign = |a| / a

Tactic:
by simp [az]

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

Goal state before:
pp: case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ (n.gcdA k % ↑k).toNat < k

Tactic:
rw [Int.toNat_lt (Int.emod_nonneg _ hk')]
    exact Int.emod_lt _ hk'

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 : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < c ↔ a - c < b

Tactic:
hb.tsub_lt_iff_left h₁,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a < b + c ↔ a - c < b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : LT α
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
simp_rw [WithBot.bot_lt_iff_ne_bot, add_ne_bot]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ a ≤ ↑(ofAdd b)

Tactic:
by
  rwa [← coe_unzero ha, coe_le_coe, ← ofAdd_toAdd (unzero ha), ofAdd_le]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := ha y hy

Goal state after:
case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
w : α
hws : w ∈ s
hwr : r x w ∧ r y w
⊢ ∃ z ∈ insert x s, r x z ∧ r y z
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
⊢ -(a + b) = b * ⅟a * b

Tactic:
rw [add_comm] at h'

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟b * a + ⅟a * b
h_a_binv_a : -(b + a) = a * ⅟b * a
⊢ -(a + b) = b * ⅟a * b
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
⊢ IsUnit 0

Tactic:
refine (ht ?_).elim

Goal state after:
case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
⊢ f t = 1