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) → motive n → motive (Nat.bit b n)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
⊢ (if n0 : Nat.bit false 0 = 0 then ⋯ ▸ zero
    else
      have x := bit (1 &&& Nat.bit false 0 != 0) (Nat.bit false 0 >>> 1) (binaryRec zero bit (Nat.bit false 0 >>> 1));
      ⋯ ▸ x) =
    bit false 0
      (if n0 : 0 = 0 then ⋯ ▸ zero
      else
        have x := bit (1 &&& 0 != 0) (0 >>> 1) (binaryRec zero bit (0 >>> 1));
        ⋯ ▸ x)

Tactic:
exact h.symm

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
⊢ flip (r ∘r p) = flip p ∘r flip r

Tactic:
by
  funext c a
  apply propext
  constructor
  · exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩
  · exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩

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 : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
induction hbc with

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
induction hbc with

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
induction hbc with

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

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝

Tactic:
apply h.symm

Goal state after:
case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • (x * a) = r • (b * x)

Tactic:
h.eq

Goal state after:
M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • (b * x) = r • (b * x)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ (x₁ • y) • z = x₁ • y • z

Tactic:
smul_eq_mul,

Goal state after:
R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • y * z = x₁ • y • z
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • z • y = x₁ • y • z

Tactic:
smul_eq_mul,

Goal state after:
R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • (z * y) = x₁ • y • z
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✝ : SMulCommClass M N N
x : M
y : N
⊢ x • y • 1 = x • y

Tactic:
smul_eq_mul,

Goal state after:
M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ x • (y * 1) = x • y
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • 1 * y) • z = x • y • z

Tactic:
smul_eq_mul,

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ x • 1 * y * z = x • y • z
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ x • y • z = y • (z * x • 1)

Tactic:
smul_eq_mul,

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ x • (y * z) = y • (z * x • 1)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ y * z * x • 1 = y • (z * x • 1)

Tactic:
smul_eq_mul,

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ y * z * x • 1 = y * (z * x • 1)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ ((m • n) • 1) • q = m • n • q

Tactic:
smul_assoc m,

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ (m • n • 1) • q = m • n • q
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_sum, not_or]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ Ord.compare x✝¹ x✝ = compareOfLessAndEq x✝¹ x✝

Tactic:
simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt,
      hf.eq_iff]

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

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

Tactic:
induction hbc with

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ Disjoint s (insert a t) ↔ ¬a ∈ s ∧ Disjoint s t

Tactic:
rw [disjoint_comm, disjoint_insert_left, disjoint_comm]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : 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)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : a ⊔ b = b
⊢ b ⊓ a = a

Tactic:
rw [← h, inf_comm, inf_sup_self]

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Nontrivial
z : α
⊢ ∃ x, x ∈ s ∧ x ≠ z

Tactic:
by_contra! H

Goal state after:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
H : ∀ (x : α), x ∈ s → x = z
⊢ False
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
by
  simp [or_iff_not_imp_right]

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ max b c

Tactic:
le_sup_iff,

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ b ∨ a ≤ c
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_sup_right

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

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

Tactic:
inf_sup_left x z y

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inr
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inr ⟨x, hx⟩

Tactic:
rw [dif_neg]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [sup_assoc]

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

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

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]
  exact disjoint_sdiff_self_left

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
        { rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff] }

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp [← symmDiff_assoc]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b

Tactic:
by simp_rw [bihimp_assoc, bihimp_comm]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)

Tactic:
rw [h.eq_bot, sdiff_bot]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
a : ι
⊢ ∃ a_1, codRestrict f (range f) ⋯ a_1 = ⟨f a, ⋯⟩

Tactic:
exact ⟨a, rfl⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
by_cases h : x ∈ s <;> [left; right] <;> use x <;> simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map f h) = Subtype.val ⁻¹' f '' {x | p x}

Tactic:
ext ⟨x, hx⟩
  simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map]
  simp only [Subtype.mk.injEq, exists_prop, mem_ofPred_eq]

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

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
⊢ toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
by
  ext x
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨rfl, hx, hx⟩
  · obtain ⟨⟨x, y⟩, h⟩ := x
    rintro ⟨rfl : x = y, h2x⟩
    exact mem_image_of_mem _ h2x.1

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ val ⁻¹' t = ∅ ↔ s ∩ t = ∅

Tactic:
by
  simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
i : γ
⊢ e₁ (e₂ i) = i

Tactic:
he₁₂

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
i : γ
⊢ e₂ i = e₂ i
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ BijOn f (s \ {a}) (t \ {f a})

Tactic:
convert! h₁.subset_left sdiff_subset
  simp [h₁.injOn.image_sdiff, h₁.image_eq, h₂, inter_eq_self_of_subset_right]

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

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

Tactic:
exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = f (fa y)
⊢ x = y

Tactic:
h.eq

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ↑(f a)) = ↑(f a)

Tactic:
extendDomain_apply_image,

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ ↑(f (g₁ (g₂ a))) = ↑(f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ↑(f a)) = ↑(f a)

Tactic:
extendDomain_apply_image,

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ ↑(f (g₂ (g₁ a))) = ↑(f a)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
h : x * y = 1
⊢ f x⁻¹ = f y

Tactic:
rw [inv, inv_eq_of_mul_eq_one_right (by rw [← mul, h, one])]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b = 0 ↔ b = 0

Tactic:
simp [ha]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b ≠ 0 ↔ b ≠ 0

Tactic:
simp [ha]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (if f z = x then y else if f z = y then x else f z) = f (if z = f⁻¹ x then f⁻¹ y else if z = f⁻¹ y then f⁻¹ x else z)

Tactic:
split_ifs <;> simp_all [eq_symm_apply]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
inst✝² : MulZeroOneClass γ
inst✝¹ : MulZeroOneClass δ
inst✝ : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ (⇑hnp ∘ ⇑hmn) 0 = 0

Tactic:
rw [comp_apply, map_zero, map_zero]

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

Goal state before:
pp: case pos
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
simp [ha]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a ^ (-1 + 1) = a ^ (-1) * a

Tactic:
simp [ha]

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
  · simp [hm]
  by_cases hn : n = 0
  · simp [hn]
  by_cases ha : a = 0
  · subst a
    simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h
    rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
  · exact zpow_add₀ ha m n

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

Goal state before:
pp: n : ℕ
h : 1 < n
⊢ n < n * n

Tactic:
have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h); grind

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Inhabited α
h : ¬Nontrivial α
x : α
H : ¬x = default
⊢ False

Tactic:
exact h ⟨_, _, H⟩

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x✝ : IsUnit 0
a : M₀
a0 : 0 * a = 1
inv_val✝ : a * 0 = 1
⊢ 0 = 1

Tactic:
by rwa [zero_mul] at a0

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ = a

Tactic:
obtain ⟨u, rfl⟩ := h

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u)⁻¹ʳ⁻¹ʳ = ↑u
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
a : M
ha : a ^ n = 1
hn : n ≠ 0
⊢ ↑(ofPowEqOne a n ha hn ^ n) = ↑1

Tactic:
simp [ha]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b

Tactic:
rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
by rw [h.neg_pow, one_pow]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
rw [← intCast, Int.cast_natCast, natCast]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
by rw [h.neg_pow, one_pow]

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

Goal state before:
pp: case inl
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Even n
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
exact Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a * a⁻¹ ≤ a * b ↔ 1 ≤ a * b

Tactic:
rw [mul_inv_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ b * a ≤ b * b⁻¹ ↔ b * a ≤ 1

Tactic:
rw [mul_inv_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ a * a⁻¹ < a * b ↔ 1 < a * b

Tactic:
rw [mul_inv_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ b * a < b * b⁻¹ ↔ b * a < 1

Tactic:
rw [mul_inv_cancel]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 1 + 0 ≤ 1 + 1

Tactic:
gcongr; exact zero_le_one

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddRightMono α
⊢ 0 + 1 ≤ 1 + 1

Tactic:
gcongr; exact zero_le_one

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

Goal state before:
pp: case inr
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a

Tactic:
exact ⟨y, h⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
obtain ha | ha := ha.eq_or_lt

Goal state after:
case inl
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2
a : α
ha✝ : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 = a
⊢ a * b ≤ a * c

case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2
a : α
ha✝ : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ a * b ≤ a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
obtain ha | ha := ha.eq_or_lt

Goal state after:
case inl
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2
a : α
ha✝ : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 = a
⊢ b * a ≤ c * a

case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2
a : α
ha✝ : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ b * a ≤ c * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < a * b

Tactic:
simpa using mul_lt_mul_of_pos_left hb ha

Goal state after: