mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: r : ArgReorder
x : Nat × ArgReorder
h✝ : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r

Tactic:
decreasing_by
  cases r; grind [→ Array.sizeOf_lt_of_mem]

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: r : ArgReorder
perm : List String :=
  List.map
    (fun x ↦
      match x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun x_1 ↦
              match x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val.attach))
    (List.attach r.perm)
x : Nat × ArgReorder
h✝ : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r

Tactic:
decreasing_by
  cases r; grind [→ Array.sizeOf_lt_of_mem]

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n ≠ 0
⊢ binaryRec' zero
      (fun b n h ih ↦
        if h' : n = 0 then
          have this := ⋯;
          ⋯ ▸ one
        else bit b n h' ih)
      (Nat.bit b n) =
    bit b n h (binaryRecFromOne zero one bit n)

Tactic:
binaryRec'_eq _ _ (by simp [h]),

Goal state after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n ≠ 0
⊢ (if h' : n = 0 then
      have this := ⋯;
      ⋯ ▸ one
    else
      bit b n h'
        (binaryRec' zero
          (fun b n h ih ↦
            if h' : n = 0 then
              have this := ⋯;
              ⋯ ▸ one
            else bit b n h' ih)
          n)) =
    bit b n h (binaryRecFromOne zero one bit n)
Module: Mathlib.Order.Defs.Unbundled

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

Tactic:
simpa using asymm a b

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
hf : FactorsThrough g f
x : α
⊢ g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x

Tactic:
simp only [comp_apply, hf.extend_apply]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : TransGen r b c
⊢ TransGen r a c

Tactic:
induction hbc with
  | single hbc => exact tail' hab hbc
  | tail _ hcd hac => exact hac.tail hcd

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
  cases h with
  | single hac => exact ⟨_, by rfl, hac⟩
  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b

Tactic:
rcases h with (rfl | h)
    · rfl
    · exact h.to_reflTransGen

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) b c

Tactic:
by
  induction hab with
  | refl => exact ⟨c, hac, refl⟩
  | @tail d e _ hde ih =>
    rcases ih with ⟨b, hdb, hcb⟩
    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
    rcases this with ⟨a, hea, hba⟩
    cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
⊢ f^[n] ∘ f = f ∘ f^[n]

Tactic:
(Commute.self_iterate f n).comp_eq

Goal state after:
α : Type u
f : α → α
n : ℕ
⊢ f^[n] ∘ f = f^[n] ∘ f
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)

Tactic:
by rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
⊢ Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

Tactic:
by
  ext x
  cases x <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

Tactic:
by
  ext x
  cases x <;> rfl

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
{ exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _) }

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ map (f₁ ∘ f₂) (g₁ ∘ g₂) a = a

Tactic:
hf.comp_eq_id,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ map id (g₁ ∘ g₂) a = a
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬IsMin a ↔ ∃ b, b < a

Tactic:
by
  simp [lt_iff_le_not_ge, IsMin, not_forall]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
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:
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)

Goal state after:
case refine_2.inl
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

case refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
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.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    ∃ a_2,
      (a.fst < a_2.fst ∧ a.snd ≤ a_2.snd ∨ a.fst ≤ a_2.fst ∧ a.snd < a_2.snd) ∧
        (a_2.fst < b.fst ∧ a_2.snd ≤ b.snd ∨ a_2.fst ≤ b.fst ∧ a_2.snd < b.snd)

Tactic:
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)

Goal state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: a b : Bool
H : a = true
⊢ (a || b) = true

Tactic:
by simp [H]

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

Goal state before:
pp: case pos
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∀ (a : α), ∃ b, ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
exact PSum.inr ⟨H⟩

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

Goal state before:
pp: m n k : ℕ
motive : (m : ℕ) → m ≤ k → Sort u_1
hmn : m ≤ n
hnk : n ≤ k
of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive k ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn

Tactic:
induction hnk with
  | refl => rw [decreasingInduction_self]
  | step hnk ih =>
      rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
⊢ (cmp a b).swap = cmp b a

Tactic:
by
  unfold cmp cmpUsing
  by_cases h : a < b <;> by_cases h₂ : b < a <;> simp_all [lt_asymm]

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ

Tactic:
exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

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

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

Tactic:
himp_self,

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

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

Tactic:
himp_self,

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

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

Tactic:
himp_self,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ ⊤ ⊓ (a ⇨ b) = b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
himp_self,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ (b ⇨ a) ⊓ ⊤ = a
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_left_comm

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

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

Tactic:
disjoint_left_comm,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint bᶜᶜ (a ⊓ (a ⊓ b)ᶜ)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by rw [sup_inf_sdiff]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [← le, ← le, map_sdiff, map_sup, sdiff_le_iff]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x

Tactic:
by rw [sup_inf_sdiff]

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

Goal state before:
pp: case pos
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

Tactic:
simp [*, Set.ite, or_iff_right_of_imp (@h x)]

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

Goal state before:
pp: case neg
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : ¬x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

Tactic:
simp [*, Set.ite, or_iff_right_of_imp (@h x)]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
⊢ z \ x ≤ z \ y ↔ y ≤ x

Tactic:
by
  refine ⟨fun h ↦ ?_, sdiff_le_sdiff_left⟩
  rw [← sdiff_sdiff_eq_self hx, ← sdiff_sdiff_eq_self hy]
  exact sdiff_le_sdiff_left h

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
α : Type u_9
β : α → Type u_10
a✝ : α
x✝ : { s // s.fst = a✝ }
a : Sigma β
h : a.fst = a✝
⊢ (fun b ↦ ⟨⟨a✝, b⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
        ⟨a, h⟩) =
    ⟨a, h⟩

Tactic:
by cases h; simp

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a \ a ∆ b = a ⊓ b

Tactic:
by simp [sdiff_symmDiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ

Tactic:
congr 1
        rw [inf_comm, inf_assoc]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
b : β
hb : f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Tactic:
exact ⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ SurjOn (g ∘ f) s (g '' t)

Tactic:
rw [SurjOn, image_comp g f]; exact image_mono hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f (invFunOn f s (f x)) = f x'

Tactic:
he,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f (invFunOn f s (f x')) = f x'
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / b * (b / c) = a / c

Tactic:
← mul_div_assoc,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / b * b / c = a / c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * (b / a) = b

Tactic:
← mul_div_assoc,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * b / a = b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit a

Tactic:
have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]

Goal state after:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit (↑u⁻¹ * (↑u * a))
⊢ IsUnit a
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)

Tactic:
rw [mk_mul_mk, mul_one]

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : MulOneClass N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

Tactic:
rw [mk_mul_mk, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
| ↑(k + 1)

Tactic:
rw [← Nat.mod_add_div (k + 1) 2]

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
| ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
| ↑(k + 1)

Tactic:
rw [← Nat.mod_add_div (k + 1) 2]

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
| ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case ind
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k → m.binCast = ↑m
⊢ k.binCast = ↑k

Tactic:
cases k with
  | zero => rw [Nat.binCast, Nat.cast_zero]
  | succ k =>
      rw [Nat.binCast]
      by_cases h : (k + 1) % 2 = 0
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
by
  rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
zero_eq_one : 0 = 1
⊢ x = 0

Tactic:
by
  rw [← one_smul R x, ← zero_eq_one, zero_smul]

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

Goal state before:
pp: a b c : ℕ
h : a = b * c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
rcases le_total b c with bc | cb
  · exact Or.inl <| le_sqrt.mpr <| h ▸ mul_le_mul_left b bc
  · exact Or.inr <| le_sqrt.mpr <| h ▸ mul_le_mul_right c cb

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:
rcases h with ⟨u, rfl⟩
  rw [inverse_unit, Units.mul_inv]

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

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

Tactic:
← mul_div_assoc,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a / b * b / c = a / c
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : CommGroup α
inst✝ : AddCommGroup β
a b : β
n : ℤ
⊢ ((zmultiplesHom β).toFun (a + b)) n = ((zmultiplesHom β).toFun a + (zmultiplesHom β).toFun b) n

Tactic:
by simp [zsmul_add]

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

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

Tactic:
rintro ⟨a, rfl⟩ ⟨b, rfl⟩
  refine ⟨a + b + 1, ?_⟩
  rw [two_mul, two_mul]
  ac_rfl

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

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[1] = f

Tactic:
iterate_one

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f = f
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)

Tactic:
calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ ≤ d * a := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

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₀
a b : G₀
ha : 0 < a
⊢ 1 < a⁻¹ * b ↔ a < b

Tactic:
by rw [lt_inv_mul_iff₀ ha, mul_one]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c ↔ a * c < b

Tactic:
rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc]

Goal state after:
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✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
← neg_mul_neg,

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ -a * -b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
obtain ha | ha := le_total a 1

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = |a|ₘ ^ n

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : |a|ₘ = b
⊢ a = b ∨ a = b⁻¹

Tactic:
by
  simpa only [← h, eq_comm (a := |a|ₘ), inv_eq_iff_eq_inv] using mabs_choice a

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

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

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

Tactic:
· rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]
    rwa [div_le_one']

Goal state after:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ max a b / min a b = |a / b|ₘ
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 < ↑k

Tactic:
exact Int.emod_lt _ hk'

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular (b * a)

Tactic:
rw [h]; exact isRegular_one.left

Goal state after: