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

Goal state before:
pp: case ind
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k' → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : k' ≠ 0
⊢ m * npowRec' k' m = npowRec' k' m * m

Tactic:
match k' with
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, ih]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 ^ (n + 1) = 1

Tactic:
by rw [pow_succ, one_pow, one_mul]

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

Goal state before:
pp: α : 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⟩
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t

Tactic:
simp only [g, cast_cast, cast_eq] at this

Goal state after:
α : 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⟩
s t : Set T
h : g s = g t
this : s = t
⊢ s = t
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
⊢ Pi.map f (update g i a) = update (Pi.map f g) i (f i a)

Tactic:
by
  ext j
  obtain rfl | hij := eq_or_ne j i <;> simp [*]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
⊢ ReflTransGen r = TransGen r

Tactic:
← transGen_reflGen,

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
⊢ TransGen (ReflGen r) = TransGen r
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
i : Option α
⊢ i.elim (f none) (f ∘ some) = f i

Tactic:
cases i

Goal state after:
case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ none.elim (f none) (f ∘ some) = f none

case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ (some val✝).elim (f none) (f ∘ some) = f (some val✝)
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
i : Option γ
⊢ (i.elim (h x) fun j ↦ h (f j)) = h (i.elim x f)

Tactic:
cases i

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
⊢ (none.elim (h x) fun j ↦ h (f j)) = h (none.elim x f)

case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
val✝ : γ
⊢ ((some val✝).elim (h x) fun j ↦ h (f j)) = h ((some val✝).elim x f)
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
i : Option γ
⊢ (i.elim (h x y) fun j ↦ h (f j) (g j)) = h (i.elim x f) (i.elim y g)

Tactic:
cases i

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
⊢ (none.elim (h x y) fun j ↦ h (f j) (g j)) = h (none.elim x f) (none.elim y g)

case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
val✝ : γ
⊢ ((some val✝).elim (h x y) fun j ↦ h (f j) (g j)) = h ((some val✝).elim x f) ((some val✝).elim y g)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using le_of_eq <| compare_eq_iff_eq.1 h

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
by
    simp_rw [Prod.lt_iff]
    rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · obtain ⟨c, ha, hb⟩ := exists_between h₁
      exact ⟨(c, _), Or.inl ⟨ha, h₂⟩, Or.inl ⟨hb, le_rfl⟩⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h₂
      exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩

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:
by
  rw [← not_iff_not, not_lt, Int.mul_nonneg_iff]
  lia

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

Goal state before:
pp: case zero
motive : (m : ℕ) → 0 ≤ m → Sort u_1
refl : motive 0 ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : 0 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

Tactic:
simp [leRec, Or.by_cases, dif_neg]

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

Goal state before:
pp: case succ
n✝ : ℕ
motive : (m : ℕ) → n✝ + 1 ≤ m → Sort u_1
refl : motive (n✝ + 1) ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n✝ + 1 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

Tactic:
simp [leRec, Or.by_cases, dif_neg]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Monotone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Monotone f

Tactic:
rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩

Goal state after:
case mp.refine_1
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ x.snd

case mp.refine_2
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ y.snd

case mp.refine_3
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ x.fst

case mp.refine_4
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ y.fst
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case succ
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
| succ c ih =>

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

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

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

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 : b ≤ a
⊢ p (max a b)

Tactic:
by
  rwa [sup_eq_left.2 h]

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

Goal state before:
pp: α : Type u
x : α
H : {x}.Nontrivial
⊢ False

Tactic:
nontrivial_iff_exists_ne (mem_singleton x)

Goal state after:
α : Type u
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
⊢ False
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
by rw [le_himp_iff, inf_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a

Tactic:
rw [← h.eq_top, sup_himp_self_left]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

Tactic:
rw [le_himp_iff, inf_right_comm, ← le_himp_iff]

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
simp_rw [inf_comm a, ← le_himp_iff, sup_le_iff, le_himp_iff, ← sup_le_iff]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ⊓ a ⊔ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ map e.symm (map e x) = x

Tactic:
convert! (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm

Goal state after:
case e'_3
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ x = map (e.trans e.symm) x
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) i = ((e.trans g).sumCongr (f.trans h)) i

Tactic:
cases i

Goal state after:
case inl
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₁
⊢ ((e.sumCongr f).trans (g.sumCongr h)) (inl val✝) = ((e.trans g).sumCongr (f.trans h)) (inl val✝)

case inr
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) (inr val✝) = ((e.trans g).sumCongr (f.trans h)) (inr val✝)
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α : Type u_9
β : Type u_10
i : α ⊕ β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) i = (Equiv.refl (α ⊕ β)) i

Tactic:
cases i

Goal state after:
case inl
α : Type u_9
β : Type u_10
val✝ : α
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) (inl val✝) = (Equiv.refl (α ⊕ β)) (inl val✝)

case inr
α : Type u_9
β : Type u_10
val✝ : β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) (inr val✝) = (Equiv.refl (α ⊕ β)) (inr val✝)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sdiff_inf_right_comm,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y) \ z = ⊥ ↔ x ⊓ y \ z = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ y ⊔ x ⊓ yᶜ = x

Tactic:
rw [← sdiff_eq, sup_inf_sdiff _ _]

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

Goal state before:
pp: case mpr.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
hai : ¬a ∈ {i}
has : a ∈ s
⊢ a ∈ Set.image (⇑(swap i j)) s

Tactic:
· exact ⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P (e.symm b)
⊢ (Equiv.piCongrLeft' P e) (update f (e.symm b) x) = update ((Equiv.piCongrLeft' P e) f) b x

Tactic:
ext b'

Goal state after:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P (e.symm b)
b' : β
⊢ (Equiv.piCongrLeft' P e) (update f (e.symm b) x) b' = update ((Equiv.piCongrLeft' P e) f) b x b'
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ s.domRestrict f '' Subtype.val ⁻¹' t = f '' (t ∩ s)

Tactic:
by
  rw [domRestrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
⊢ ∃ a, const α a = f

Tactic:
rcases isEmpty_or_nonempty α with h | ⟨⟨a⟩⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
h : IsEmpty α
⊢ ∃ a, const α a = f

case inr
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
a : α
⊢ ∃ a, const α a = f
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
⊢ pullbackDiagonal f ∩ Subtype.val ⁻¹' univ = pullbackDiagonal f

Tactic:
preimage_univ,

Goal state after:
X : Type u_1
Y : Sort u_2
f : X → Y
⊢ pullbackDiagonal f ∩ univ = pullbackDiagonal f
Module: Mathlib.Data.Set.Function

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

Tactic:
have : y = z := by
    apply hf (hs ys) (ht zt)
    rwa [← hz] at hy

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅

Tactic:
← hf.image_inter hs ht,

Goal state after:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ p₂ (f a) = g (p₁ a)

Tactic:
rw [comm a]

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

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((- -[m+1] - 1) / (↑n + 1) + 1)

Tactic:
rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]; rw [Int.add_sub_cancel]; rfl

Goal state after:
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 : Injective 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
n : ℕ
x : M₁
⊢ f (x ^ ↑n.succ) = f (x ^ ↑n * x)

Tactic:
rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]

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

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

Tactic:
rw [mul_inv_eq_one, mul_eq_left]

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

Goal state before:
pp: α : 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 : α
⊢ r b c → p a b → p b c → p a c → f a c = f a b * f b c

Tactic:
rbc

Goal state after:
α : 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
⊢ p a b → p b c → p a c → f a c = f a b * f b c
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
⊢ 1 x = 0 ↔ x = 0

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 0 ↔ 0 = 0

case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 0 ↔ x = 0
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
⊢ 1 x = 1 ↔ x ≠ 0

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 1 ↔ 0 ≠ 0

case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 1 ↔ x ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x y : β
⊢ g • x * g • y⁻¹ = g • x * (g • y)⁻¹

Tactic:
smul_inv₀'

Goal state after:
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x y : β
⊢ g • x * (g • y)⁻¹ = g • x * (g • y)⁻¹
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ m ∣ b ^ n

Tactic:
trans (a ^ n) <;> [gcongr; apply_rules [pow_dvd_pow_of_dvd]]

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

Goal state before:
pp: 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
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c → (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)

Tactic:
bc

Goal state after:
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
⊢ μ a b ≤ μ a c
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✝ : MulRightMono α
h : a * b < c * d
⊢ a < max c d ∨ b < max c d

Tactic:
lt_max_iff

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ (a < c ∨ a < d) ∨ b < c ∨ b < d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MulOneClass α
inst✝ : LE α
a b : α
⊢ 1 * a ≤ 1 * b → a ≤ b

Tactic:
simpa only [one_mul] using id

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ c + a ≤ c + b

Tactic:
rw [add_comm c, add_comm c]; exact add_le_add_left a b h c

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd✝ : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
exact (mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a * b < 0

Tactic:
rcases lt_trichotomy 0 a with (ha | rfl | ha)

Goal state after:
case inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a * b < 0

case inr.inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0

case inr.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
neg_pos,

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < a ∧ b < 0 ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
⊢ s (e x) (e (e.symm y)) ↔ s (e x) y

Tactic:
e.apply_symm_apply

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
⊢ s (e x) y ↔ s (e x) y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ s (e (e.symm x)) (e y) ↔ s x (e y)

Tactic:
e.apply_symm_apply

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ s x (e y) ↔ s x (e y)
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
x : α
y : β
⊢ e x < e (e.symm y) ↔ e x < y

Tactic:
e.apply_symm_apply

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
x : α
y : β
⊢ e x < y ↔ e x < y
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ Codisjoint (f a) (f b)

Tactic:
by
  rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]
  exact f.monotone ha.top_le

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.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ max a a⁻¹ = a⁻¹ ↔ a ≤ 1

Tactic:
max_eq_right_iff,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ a ≤ a⁻¹ ↔ a ≤ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
by rw [sup_div_inf_eq_mabs_div]

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

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

Tactic:
by
  constructor <;> rintro ⟨x, h⟩
  · exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩
  · exact ⟨x, mod_cast h⟩

Goal state after: