mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : α
h : f x = f y
⊢ x = y

Tactic:
by
  obtain ⟨x, rfl⟩ := hg x
  obtain ⟨y, rfl⟩ := hg y
  exact congr_arg g (I h)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
a b : α
hab : r a b
⊢ SymmGen (Function.swap r) a b

Tactic:
| inr hab =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
a b : α
h : ReflTransGen r a b
⊢ r a b

Tactic:
by
      induction h with
      | refl => exact refl a
      | tail _ h₂ IH => exact IsTrans.trans _ _ _ IH h₂

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ y = x ∨ TransGen r x y

Tactic:
reflGen_iff

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen r ≤ EqvGen r

Tactic:
intro _ _ h
  induction h using TransGen.trans_induction_on with
  | trans _ _ h1 h2 => exact _root_.trans h1 h2
  | single h => exact .rel _ _ h

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c

Tactic:
· cases h

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d

pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d

Tactic:
· cases h

Goal state after:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a ⋯ ∈ pmap f x h

Tactic:
rw [mem_def] at ha ⊢
  subst ha
  rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap < (b, a) ↔ x < (a, b)

Tactic:
rw [← swap_lt_swap]; simp

Goal state after:
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 : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
⊢ False

Tactic:
rcases hne.1.lt_or_gt with h₁ | h₁ <;>
  rcases hne.2.1.lt_or_gt with h₂ | h₂

Goal state after:
case inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False

case inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False

case inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False

case inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x y H
    rwa [leRecOn_self, leRecOn_self] at H

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a ≤ f b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
hf.le_iff_le ha hb,

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a ≤ b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: ⊢ Monotone fun n ↦ n ^ n

Tactic:
refine monotone_nat_of_le_succ fun n ↦ ?_

Goal state after:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ (n + 1)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case ofNat
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn (ofNat n) f fun n ↦ g (n + 1)) < casesOn (ofNat n + 1) f fun n ↦ g (n + 1)

pp: case negSucc.zero
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (casesOn -[0+1] f fun n ↦ g (n + 1)) < casesOn (-[0+1] + 1) f fun n ↦ g (n + 1)

pp: case negSucc.succ
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn -[n + 1+1] f fun n ↦ g (n + 1)) < casesOn (-[n + 1+1] + 1) f fun n ↦ g (n + 1)

Tactic:
· exact hf n.lt_succ_self

Goal state after:
case negSucc.zero
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (casesOn -[0+1] f fun n ↦ g (n + 1)) < casesOn (-[0+1] + 1) f fun n ↦ g (n + 1)

case negSucc.succ
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn -[n + 1+1] f fun n ↦ g (n + 1)) < casesOn (-[n + 1+1] + 1) f fun n ↦ g (n + 1)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
⊢ f n = f b

Tactic:
obtain ⟨m, hmb, hm⟩ : ∃ m ≤ b, f m = f (m + 1) := by
    contrapose! hfb
    let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
    | 0, _ => Nat.zero_le _
    | m + 1, hmb => (strictMono _ <| m.le_succ.trans hmb).trans_lt <| (hfmono m.le_succ).lt_of_ne <|
        hfb _ <| Nat.le_of_succ_le_succ hmb
    exact ⟨b + 1, strictMono _ le_rfl⟩
  replace key : ∀ k : ℕ, f (m + k) = f (m + k + 1) ∧ f (m + k) = f m := fun k =>
    Nat.rec ⟨hm, rfl⟩ (fun k ih => ⟨hfstab _ ih.1, ih.1.symm.trans ih.2⟩) k
  replace key : ∀ k ≥ m, f k = f m := fun k hk =>
    (congr_arg f (Nat.add_sub_of_le hk)).symm.trans (key (k - m)).2
  exact (key n (hmb.trans hbn)).trans (key b hmb).symm

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ {x | x ∈ l} = {a} ↔ ∃ n, n > 0 ∧ l = List.replicate n a

Tactic:
simpa +contextual [Set.ext_iff, iff_iff_implies_and_implies, forall_and, List.eq_replicate_iff,
    List.length_pos_iff_exists_mem] using ⟨fun _ _ ↦ ⟨_, ‹_›⟩, fun x hx h ↦ h _ hx ▸ hx⟩

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ a

Tactic:
rw [partial_order_eq]
      apply inf_le_left

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

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

Tactic:
sdiff_le_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ c ↔ a ≤ c ⊔ b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sdiff_le_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ≤ a \ c ⊔ c \ b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sdiff_le_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a \ c ⊔ c \ b)
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sdiff_le_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ b ⊔ (c ⊔ d) ↔ a ≤ b ⊔ c ⊔ d
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sdiff_le_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ c ⊔ (a \ b ⊔ b \ c)
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sdiff_le_iff,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ∧ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ c
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
⊢ y ⊔ y \ x ≤ y \ x ⊔ x ⊔ z

Tactic:
grind [sup_of_le_left, sdiff_le', le_sup_left, sdiff_sup_self']

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

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
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ ∀ (a : β), q a ↔ p (e.symm a)

Tactic:
by as_aux_lemma => grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ g (e (e.symm b)) ≍ g b

Tactic:
exact congr_arg_heq _ (e.apply_symm_apply _)

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 ⊓ b) ≤ a ∆ c ⊔ b ∆ c

Tactic:
rw [sdiff_inf]
    exact sup_le_sup le_sup_right le_sup_right

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = ∅ ↔ IsEmpty ι

Tactic:
rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ univ.pi t = {a} ↔ ∀ (i : ι), t i = {a i}

Tactic:
by
  classical
  simp only [eq_singleton_iff_unique_mem]
  refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
  rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
⊢ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

Tactic:
intro x hx y hy hxy
    obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
    exact h.le_bot ⟨hx, hy⟩

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

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

Tactic:
update_of_ne h

Goal state after:
case refine_2.inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ f j ∈ t j
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
· intro h
      have : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
      exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
show f (x * y) * g (x * y) = f x * g x * (f y * g y)

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g⁻¹ * g ^ (-↑n))
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 : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c

Tactic:
obtain rab | rba := total_of r a b

Goal state after:
case inl
α : 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
rab : r a b
⊢ f a c = f a b * f b c

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
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u a : αˣ
⊢ a ^ 0 = 1

Tactic:
by simp only [HPow.hPow, Pow.pow]; simp

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a / b * b = a

Tactic:
by
  rw [div_eq_mul_inv, h.inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b / b = a

Tactic:
by
  rw [div_eq_mul_inv, h.mul_inv_cancel_right]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext <;> apply mul_comm

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

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
p : Prop
inst✝ : Decidable p
a : M₀
b : A
⊢ (if p then a else 0) • b = if p then a • b else 0

Tactic:
by
  rw [ite_smul, zero_smul]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : 0 ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ 0 ^ (m + n) = 0 ^ m * 0 ^ n

Tactic:
simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 ^ (m + n) = 0 ^ m * 0 ^ n
Module: Mathlib.Data.List.TFAE

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

Tactic:
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: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x * x⁻¹ʳ = 1

Tactic:
by
  rcases h with ⟨u, rfl⟩
  rw [inverse_unit, Units.mul_inv]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : x⁻¹ʳ * y = z
⊢ y = x * (x⁻¹ʳ * y)

Tactic:
mul_inverse_cancel_left _ _ h

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : x⁻¹ʳ * y = z
⊢ y = y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) ⋯

Tactic:
simp_rw [val_mk0]

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

Goal state before:
pp: M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
⊢ f = g

Tactic:
ext (x | x)
  · exact (DFunLike.congr_fun h_nat x :)
  · rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
    congr 1
    exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
h : IsUnit 2
a : α
⊢ Odd a

Tactic:
rw [← sub_add_cancel a 1]
  exact (Even.of_isUnit_two h _).add_one

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

Goal state before:
pp: case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1

Tactic:
rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (c + b) = a - c - b

Tactic:
apply tsub_add_eq_tsub_tsub

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 - a ≤ (1 - b) * (1 + c)

Tactic:
by
  rw [one_sub_mul, mul_one_add, sub_le_sub_iff, add_assoc, add_comm c]
  gcongr

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b

Tactic:
le_mul_inv_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c ≤ b ↔ c * a ≤ b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ↪r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ {a b : α}, i.toEmbedding b ≤ i.toEmbedding a ↔ b ≤ a

Tactic:
by rw [forall_comm]; exact @i.2

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ↪r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ {a b : α}, i.toEmbedding a ≤ i.toEmbedding b ↔ a ≤ b

Tactic:
by rw [forall_comm]; exact @i.2

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ {a b : α}, i.toEquiv b ≤ i.toEquiv a ↔ b ≤ a

Tactic:
by rw [forall_comm]; exact @i.2

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ≃r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ {a b : α}, i.toEquiv a ≤ i.toEquiv b ↔ a ≤ b

Tactic:
by rw [forall_comm]; exact @i.2

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b ≤ a ↔ b ≤ f a

Tactic:
convert! (map_le_map_iff f).symm

Goal state after:
case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = f (EquivLike.inv f b)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
n : ℕ
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
simpa using pow_le_pow_right' ha (Nat.one_le_iff_ne_zero.2 hn)

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

Goal state before:
pp: x y : ℕ
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])

Goal state after:
x y : ℕ
this : x.P y (x.xgcdAux 1 0 y 0 1)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = if ↑a ≤ ↑b then ↑b else ↑a

Tactic:
val_le_val,

Goal state after:
α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = if a ≤ b then ↑b else ↑a
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊓ b) = if ↑a ≤ ↑b then ↑a else ↑b

Tactic:
val_le_val,

Goal state after:
α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊓ b) = if a ≤ b then ↑a else ↑b
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 : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + c + (b - c)

Tactic:
by rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]

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 : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c

Tactic:
by
  rw [add_comm]
  exact ha.le_tsub_iff_left h

Goal state after: