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

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

Tactic:
Nat.mul_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * n + m) = (a ^ m) ^ (n + 1)
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : α = β
a : α
c : γ
⊢ cast e a ≍ c ↔ a ≍ c

Tactic:
subst e; rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : β = γ
a : α
b : β
⊢ a ≍ cast e b ↔ a ≍ b

Tactic:
subst e; rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d

Tactic:
· exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| @tail b c _ hbc ih =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case rel
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ a b : α
h : r a b
⊢ EqvGen p a b

Tactic:
| rel a b h =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
fab : α → β
fbc : β → γ
ga : α → α
gb : β → β
gc : γ → γ
hab : Semiconj fab ga gb
hbc : Semiconj fbc gb gc
x : α
⊢ (fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)

Tactic:
simp only [comp_apply, hab.eq, hbc.eq]

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

Goal state before:
pp: R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
⊢ FaithfulSMul R A ↔ Injective fun r ↦ r • 1

Tactic:
refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
  · simp only at hr
    rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
  · simpa using hr 1

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • 1 * y = x • y

Tactic:
by rw [smul_mul_assoc, one_mul]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ (∃ a, IsEmpty β) ↔ ∃ x, True ∧ IsEmpty β

Tactic:
true_and

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ (∃ a, IsEmpty β) ↔ ∃ x, IsEmpty β
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → InvOneClass (f i)
x✝ : I
⊢ 1⁻¹ x✝ = 1 x✝

Tactic:
exact inv_one

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvOneMonoid (f i)
x✝ : I
⊢ 1⁻¹ x✝ = 1 x✝

Tactic:
exact inv_one

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.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
⊢ ∃ a, g a = d

Tactic:
by
      inhabit γ
      obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
      exact ⟨b, congr_arg Prod.snd h⟩

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

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

Tactic:
cases o <;> simp only [Ordering.Compares]

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

case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
⊢ ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
i

Goal state after:
case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
⊢ Disjoint (f i) (g i)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
⊢ x ≤ ⊥

Tactic:
i

Goal state after:
case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ ¬a ⊓ b = a ⊔ b ↔ a ≠ b

Tactic:
inf_eq_sup

Goal state after:
α : Type u
inst✝ : Lattice α
a b : α
⊢ ¬a = b ↔ a ≠ b
Module: Mathlib.Order.Lattice

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

Tactic:
simp only [inf_assoc, sup_inf_right]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a : α
⊢ ⊥ ≤ a

Tactic:
rw [← inf_inf_sdiff a a, inf_assoc]

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a : α
⊢ a ⊓ (a ⊓ a \ a) ≤ a
Module: Mathlib.Logic.Equiv.Option

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

Tactic:
by
  rcases h : e (some x) with a | a
  · rw [removeNone_none _ h]
    simpa using (congr_arg e.symm h).symm
  · rw [removeNone_some _ ⟨a, h⟩]
    have h1 := congr_arg e.symm h
    rw [symm_apply_apply] at h1
    simp only [apply_eq_iff_eq, reduceCtorEq]
    simp [h1]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ ⊥ = a
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) ∆ b = a ⊔ b

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ∆ (a \ b) = a ⊔ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b

Tactic:
sdiff_symmDiff_eq_sup,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊓ b) ∆ (a ∆ b) = a ⊔ b

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ (￢a) = ⊤

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ (￢a) = ⊤

Tactic:
by rw [symmDiff_comm, hnot_symmDiff_self]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ∆ a \ b = a \ b
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b \ b ∆ a = a ⊓ b
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ≤ b ∆ a ↔ Disjoint a b
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
inst✝¹ : DecidableEq α✝
α : Type u_9
inst✝ : Nontrivial α
⊢ Nontrivial (Perm α)

Tactic:
classical
  obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
  exact Function.Injective.nontrivial (Equiv.swap_injective_of_left a)

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ (a ∆ b) = b
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ∆ a = b ↔ a = ⊥
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
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ (s₁ ×ˢ t₁).Nonempty

Tactic:
rwa [← heq]

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

Goal state before:
pp: α : Type u_1
⊢ range Function.diag = diagonal α

Tactic:
ext ⟨x, y⟩
  simp [diagonal, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
x y : ↑(range f)
h : x < y
⊢ f (rangeSplitting f x) < f (rangeSplitting f y)

Tactic:
simpa [apply_rangeSplitting f]

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:
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: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
cases isEmpty_or_nonempty (α i)

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : IsEmpty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

case inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : Nonempty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
⊢ ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i

Tactic:
i

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
⊢ i ∈ s → t₁ i ⊆ t₂ i
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2.inl.inl
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y

pp: case refine_2.inl.inr
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y

pp: case refine_2.inr.inl
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y

pp: case refine_2.inr.inr
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y

Tactic:
exacts [h₁ hx hy hxy, (h₁₂ _ hx _ hy hxy).elim, (h₁₂ _ hy _ hx hxy.symm).elim, h₂ hx hy hxy]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (s ∪ {a}) ↔ InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
injOn_union (disjoint_singleton_right.2 has)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ (InjOn f s ∧ InjOn f {a} ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ {a} → f x ≠ f y) ↔ InjOn f s ∧ ¬f a ∈ f '' s
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ (n + 1)) = f a ^ (n + 1)

Tactic:
by rw [pow_succ, pow_succ, map_mul, map_pow f a n]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ

Tactic:
ext x
  rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
  · simp only [mem_preimage, mem_union, mem_compl_iff, mem_range_self, not_true, or_false,
      leftInverse_invFun hf _, hf.mem_set_image]
  · simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]

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

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

Tactic:
rw [div_mul_eq_div_div_swap]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
by
  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
  simp only [mul_comm, eq_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit a
⊢ a * b = a * 1 ↔ b = 1

Tactic:
rw [h.mul_right_inj]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ x * a
⊢ (fun x ↦ x * a) (a * ⋯.choose) = (fun x ↦ x * a) 1

Tactic:
by simpa [mul_assoc] using congr_arg (a * ·) (h.2 1).choose_spec

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ofSubtype x = ofSubtype y
⊢ x = y

Tactic:
Perm.ext_iff

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ∀ (x_1 : α), (ofSubtype x) x_1 = (ofSubtype y) x_1
⊢ ∀ (x_1 : Subtype p), x x_1 = y x_1
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M✝ : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁴ : AddZeroClass A
inst✝³ : DistribSMul M✝ A
R : Type u_12
S : Type u_13
M : Type u_14
inst✝² : AddZeroClass M
inst✝¹ : DistribSMul R M
inst✝ : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
c : R
x y : M
⊢ f c • (x + y) = f c • x + f c • y

Tactic:
by simp only [hsmul, smul_add]

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

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

Tactic:
unfold subNatNat
  cases e : n - m
  · simp [Nat.le_of_sub_eq_zero e]
  · rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]

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

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

Tactic:
cast_subNatNat,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑m - ↑n.succ = ↑↑m + ↑-[n+1]
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
cast_subNatNat,

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : ℕ
a : α
⊢ n • a = ↑n * a

Tactic:
induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

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

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

Tactic:
by rw [this]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -b / a = -(b / a)

Tactic:
neg_eq_neg_one_mul,

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -1 * b / a = -(b / a)
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(n + 1)) x

Tactic:
rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x

Tactic:
by
  induction n with
  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a - b) * (a + b)

Tactic:
rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Module ℕ M
n : ℕ
⊢ ∀ (m : M), n • m = n • m

Tactic:
convert! nat_smul_eq_nsmul P n

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

Goal state before:
pp: case inr
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
⊢ 0 ≤ a ^ 2

Tactic:
have hb : 0 < b := not_le.1 fun hb ↦ (add_neg_of_neg_of_nonpos ha hb).ne' hab

Goal state after:
case inr
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ 0 ≤ a ^ 2
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
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a

Tactic:
rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right h₂]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ DenselyOrdered αˣ

pp: case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
⊢ DenselyOrdered α

Tactic:
· refine ⟨fun x y h ↦ ?_⟩
    obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)
    refine ⟨Units.mk0 z (ne_zero_of_lt hz.1), by simp [← Units.val_lt_val, hz]⟩

Goal state after:
case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
⊢ DenselyOrdered α
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
x y : WithBot α
⊢ x < y ↔ x ≤ y ∧ ¬y ≤ x

Tactic:
cases x <;> cases y <;> simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
intro a b hab

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Order.Directed

Goal state before:
pp: β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
⊢ ¬IsMin b

Tactic:
intro hb'

Goal state after:
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
⊢ False
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
intro a b hab

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ ↑x * y + x.neg * y = 0

Tactic:
by simp [← add_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ x.neg * y + ↑x * y = 0

Tactic:
by simp [← add_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Invertible 2
⊢ ⅟2 + ⅟2 = 1

Tactic:
rw [← two_mul, mul_invOf_self]

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)

Tactic:
by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
⊢ StrictMono fun a ↦ a ^ n

Tactic:
intro a b hab

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f s t ⊆ image2 f s' t'

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ f a b ∈ image2 f s' t'