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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ binaryRec' zero bit 0 = zero

Tactic:
by
  rw [binaryRec', binaryRec_zero]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = b

Tactic:
by
  rw [← mul_assoc, inv_mul_cancel, one_mul]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl.refl
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
f₂ : (a : α₁) → β₁ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂
hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₁

Tactic:
cases hf rfl .rfl

Goal state after:
case refl.refl.refl
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂
hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₁
⊢ f₁ a₁ ≍ f₁ a₁
Module: Mathlib.Logic.Relation

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

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y : α
⊢ ReflTransGen r x x

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
refl : ∀ (a : α), motive ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive ⋯

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1.refl
α : Type u_1
r : α → α → Prop
a : α
⊢ a = a ∨ TransGen r a a

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
⊢ ReflTransGen (Function.swap r) i✝ i✝

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ x✝ : α
⊢ EqvGen p x✝ x✝

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
i✝¹ i✝ a✝ : α
⊢ EqvGen r a✝ a✝

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : 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
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) a c

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : 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
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r d a

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.refl
α : 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
hac : ReflTransGen r a c
d e : α
a✝¹ : ReflTransGen r a d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
hea : ReflTransGen r e f
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.refl
α : 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
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
hea : ReflTransGen r e b
⊢ Join (ReflTransGen r) e c

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ : α
⊢ r x✝ x✝

Tactic:
| refl =>

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (m • n) • p = m • n • p

Tactic:
simp_rw [← (smul_left_injective' (α := Q)).eq_iff, smul_assoc]

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

Goal state before:
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 Or.inr (Or.inr <| Lex.left _ _ hji) }

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_lt]

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✝¹ : LE α
inst✝ : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x✝¹ x✝ : α
⊢ x✝¹ < x✝ ↔ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹

Tactic:
by
    rw [← le, ← le, ← lt, lt_iff_le_not_ge]

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 α

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

Tactic:
· exact PSum.inr ⟨H⟩

Goal state after:
case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
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:
| refl =>

Goal state after:
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 : ℕ), Surjective next
⊢ Surjective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
| refl =>

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

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

Tactic:
| refl =>

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

Goal state before:
pp: case refl
a b c d e m✝ n✝ k : ℕ
p : ℕ → Prop
n m : ℕ
motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1
of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k ⋯
self : motive m ⋯
⊢ motive m ⋯

Tactic:
| refl =>

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

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

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
refine Acc.intro (a', b) fun x hx => ?_

Goal state after:
case ind.ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
⊢ Acc (fun x1 x2 ↦ x1 < x2) x
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case refl
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
⊢ r (f b) (f b.succ)

Tactic:
| refl =>

Goal state after:
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:
by
  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.Basic

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

Tactic:
rwa [Subsingleton.elim y x]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
⊢ Monotone f

Tactic:
by
  intro x y hxy
  rw [← sup_eq_right.2 hxy]
  apply h

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

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

Tactic:
sdiff_sup_cancel hbc

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hac : c ≤ a
hbc : c ≤ b
h : a \ c = b \ c
⊢ b = b
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
removeNone_none _ h

Goal state after:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ e none = e none ↔ e.symm none = some x
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ ⊥ = a

Tactic:
rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff_right_inj]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (preimage f) ↔ Injective f

Tactic:
← Surjective.of_comp_iff _ Set.ofPred_bijective.surjective,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (preimage f ∘ ofPred) ↔ Injective f
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁

Tactic:
by
  constructor
  · intro heq
    have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
    rw [prod_nonempty_iff] at h h₁
    rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
  · grind

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
⊢ map_fst ⁻¹' pullbackDiagonal f = pullbackDiagonal snd

Tactic:
by
  ext ⟨⟨p₁, p₂⟩, he⟩
  simp_rw [pullbackDiagonal, mem_ofPred, Subtype.ext_iff, Prod.ext_iff]
  exact (and_iff_left he).symm

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

Goal state before:
pp: case mpr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
· rintro (((⟨h0, h1, h2⟩ | ⟨h0, h1, h2⟩) | ⟨h0, h1⟩) | ⟨h0, h1⟩) <;>
      simp [*, h.ne_of_mem, Ne.symm]

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

Goal state before:
pp: case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → s ∩ t ⊆ s ∩ u

pp: case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u

Tactic:
· rw [← image_preimage_coe, ← image_preimage_coe]
    exact image_mono

Goal state after:
case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' (s \ t) = f '' s \ f '' (s ∩ t)

Tactic:
by
  refine subset_antisymm (subset_sdiff.2 ⟨image_mono sdiff_subset, ?_⟩)
    (sdiff_subset_iff.2 (by rw [← image_union, inter_union_sdiff]))
  exact Disjoint.image disjoint_sdiff_inter h sdiff_subset inter_subset_left

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 = 1

Tactic:
rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]

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:
Int.add_sub_cancel

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -(↑m / (↑n + 1) + 1)
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ * u₂⁻¹) = ↑u₁ * ↑u₂⁻¹

Tactic:
Units.val_mul

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * ↑u₂⁻¹ = ↑u₁ * ↑u₂⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
Units.val_mul

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ ↑v * ↑u⁻¹ = ↑v * ↑u⁻¹
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
⊢ ↑(u⁻¹ * v) = ↑u⁻¹ * ↑v

Tactic:
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
⊢ ↑u⁻¹ * ↑v = ↑u⁻¹ * ↑v
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
Prod.mk_inj

Goal state after:
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
Prod.mk_inj

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case pos
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx

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:
rw [Iff.comm, ← mul_left_inj' hb, one_mul]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
if_pos h,

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ((k + 1) / 2).binCast + ((k + 1) / 2).binCast = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a * a⁻¹ = a

pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a

Tactic:
· rw [h, inv_zero, mul_zero]

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a⁻¹ * a = a

pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a

Tactic:
· rw [h, inv_zero, mul_zero]

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a⁻¹ * a * a = a

pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a

Tactic:
· rw [h, inv_zero, mul_zero]

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x

Tactic:
rw [smul_sub, Convex.combo_self h]

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

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℤ
⊢ ↑n * a = a * ↑n

Tactic:
(n.cast_commute a).eq

Goal state after:
α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℤ
⊢ a * ↑n = a * ↑n
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (2 * c) = a ^ (2 * c)

Tactic:
zpow_mul,

Goal state after:
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ ((-a) ^ 2) ^ c = (a ^ 2) ^ c
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
add_left_comm,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
add_left_comm,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c ≤ c - b + (a + (b - a))
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
⊢ b * a ≤ c * a

Tactic:
rw [← le, mul, mul]; exact mul_le_mul_of_nonneg_right (le.2 hbc) (by rwa [← zero, le])

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

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a b : α
inst✝ : MulLeftReflectLE α
h : a ≤ b
⊢ ∃ c, 1 ≤ c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h; exact ⟨c, one_le_of_le_mul_right h, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
h : 1 < a * a
⊢ 1 < a

Tactic:
contrapose! h; exact mul_le_one' h h

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
by
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, hab, hcd, true_and]
  refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
  · exact (mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)
  · exact (mul_lt_mul_of_pos_left hcd a0).trans_le (mul_le_mul_of_nonneg_right hab d0.le)

Goal state after:
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) = d * b

Tactic:
add_left_comm,

Goal state after:
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
⊢ d * b + (c * a + d * a) = d * b
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✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) = b * d

Tactic:
add_left_comm,

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