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

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

Tactic:
case neg =>
    rw [binaryRec, dif_neg h']
    change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
    generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 1 = a

Tactic:
rw [zpow_ofNat, pow_one]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b c : α
⊢ ((∃ h, a = c) ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c

Tactic:
rw [exists_prop, exists_prop]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b c : α
⊢ ((∃ h, a = c) ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c

Tactic:
by rw [exists_prop, exists_prop]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α default

Tactic:
exact x

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

Goal state before:
pp: α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
⊢ f ≍ f'

Tactic:
have : ∀ a, f a ≍ f' a := fun a ↦ h a a (HEq.refl a)

Goal state after:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
⊢ f ≍ f'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b

Tactic:
subst h

Goal state after:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → β
x : α
y : γ
⊢ (r ∘r fun x1 x2 ↦ x1 = f x2) x y ↔ r x (f y)

Tactic:
simp [Comp]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → α
x : γ
y : β
⊢ ((fun x1 x2 ↦ f x1 = x2) ∘r r) x y ↔ r (f x) y

Tactic:
simp [Comp]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single.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✝ : IsTrans α r
a c : α
h₂ : r a c
⊢ ReflGen r a c

pp: case single.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₂ : r b c
h₁ : r a b
⊢ ReflGen r a c

Tactic:
· exact single h₂

Goal state after:
case single.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₂ : r b c
h₁ : r a b
⊢ ReflGen r a c
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.head
α : 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 ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
exact fun h1 h2 ↦ head h1 (h2.tail hbc)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr.inl
α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

pp: case mpr.inr
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Tactic:
· rfl

Goal state after:
case mpr.inr
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inl
α : Type u_1
r : α → α → Prop
b : α
⊢ ReflTransGen r b b

pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Tactic:
· rfl

Goal state after:
case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b
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:
| symm =>

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

Goal state before:
pp: α β : Sort u_1
h : α = β
a : α
b : β
⊢ (Equiv.cast h) a = b ↔ a ≍ b

Tactic:
subst h

Goal state after:
α : Sort u_1
a b : α
⊢ (Equiv.cast ⋯) a = b ↔ a ≍ b
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
subst h

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
j : ι
x : M j
y : N j
⊢ f' j (mulSingle j x j) (mulSingle j y j) = mulSingle j (f' j x y) j
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
y : α
hy : y ∈ {x}
hya : y ≠ x
⊢ False

Tactic:
exact hya (mem_singleton_iff.1 hy)

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

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

Tactic:
conv_lhs => rw [← inf_sdiff_left]

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

Goal state before:
pp: case inl
α✝ : 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.17
β : Type ?u.16
inst✝ : IsEmpty β
val✝ : α
⊢ inl (Sum.elim id (fun a ↦ isEmptyElim a) (inl val✝)) = inl val✝

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.17
β : Type ?u.16
inst✝ : IsEmpty β
x : β
⊢ inl (Sum.elim id (fun a ↦ isEmptyElim a) (inr x)) = inr x

Tactic:
· rfl

Goal state after:
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.17
β : Type ?u.16
inst✝ : IsEmpty β
x : β
⊢ inl (Sum.elim id (fun a ↦ isEmptyElim a) (inr x)) = inr x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
bot_inf_eq

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sdiff_inf, (sdiff_eq_bot_iff (α := α)).2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]

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

Goal state before:
pp: case neg
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : ¬p a
⊢ x a = x a

Tactic:
· rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [← symmDiff_of_le ha]
  exact ((symmDiff_right_involutive a).toPerm _).eq_symm_apply.symm.trans eq_comm

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

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

Tactic:
have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
⊢ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (s.piecewise f₁ f₂) (s₁ ∩ s)

pp: case refine_2
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₂ (s.piecewise f₁ f₂) (s₂ ∩ sᶜ)

Tactic:
exacts [(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right,
    (piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = s₁ ∧ True ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t = ∅) ↔ s = s₁

Tactic:
ht.ne_empty,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = s₁ ∧ True ∨ (s = ∅ ∨ False) ∧ (s₁ = ∅ ∨ False) ↔ s = s₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s → x✝ ∈ range fun x ↦ f ↑x

Tactic:
rintro ⟨x, h1, h2⟩
    exact ⟨⟨x, h1⟩, h2⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ t j (update f i a j) = t j (f j)

Tactic:
rw [update_of_ne]

Goal state after:
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ j ≠ i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi t
⊢ update a i b ∈ s.pi t ↔ i ∈ s → b ∈ t i

Tactic:
rw [update_mem_pi_iff, and_iff_right]
  exact fun j hj => ha j hj.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : ↑s → β
hf : Injective f
⊢ ∃ f, InjOn f s

Tactic:
lift f to α → β using trivial
    exact ⟨f, injOn_iff_injective.2 hf⟩

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 : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ y, f y = x) ↔ (f ⋯.choose).2 = x.2

Tactic:
refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ y, f y = x) → (f ⋯.choose).2 = x.2
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t \ {f a}
⊢ BijOn f s t

Tactic:
sdiff_singleton_eq_self hfa,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
⊢ BijOn f s t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬f x = f a

Tactic:
rw [h.injOn.eq_iff (by simp [hx]) (by simp)]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬x = a
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a' h

Tactic:
by
  cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ ≍ f a' h

Tactic:
by
  cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
h : a ≍ a'
⊢ a = a'

Tactic:
by
  cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α β : Sort u
a : α
b : β
h : a ≍ b
⊢ a = cast ⋯ b

Tactic:
by
  cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α β : Sort u
a : α
b : β
h : a ≍ b
⊢ cast ⋯ a = b

Tactic:
by
  cases h; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * Int.negSucc n) = (a ^ ↑m) ^ Int.negSucc n

Tactic:
rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = b⁻¹ ↔ a = 1

Tactic:
by rw [div_eq_mul_inv, mul_eq_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
⊢ IsUnit a → IsUnit (a ^ n)

Tactic:
rintro ⟨u, rfl⟩; exact ⟨u ^ n, rfl⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
ha : IsUnit a
⊢ IsUnit (↑ha.unit * b) ↔ IsUnit b

Tactic:
simp [-IsUnit.unit_spec]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
hb : IsUnit b
⊢ IsUnit (a * ↑hb.unit) ↔ IsUnit a

Tactic:
simp [-IsUnit.unit_spec]

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

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

Tactic:
ext <;> exact div_eq_mul_inv ..

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> f <$> y = (fun x ↦ x ∘ f) <$> x <*> y

Tactic:
simp only [← pure_seq]
  simp only [seq_assoc, seq_pure, ← comp_map]
  simp [pure_seq]
  rfl

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

Goal state before:
pp: case inl
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Subsingleton α
⊢ ∃ b, a * b = 1

pp: case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
⊢ ∃ b, a * b = 1

Tactic:
· exact ⟨a, Subsingleton.elim _ _⟩

Goal state after:
case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
⊢ ∃ b, a * b = 1
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 α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ (↑(↑f * ↑g)).toFun 0 = 0

Tactic:
dsimp; rw [map_zero, zero_mul]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / 0 = 0

Tactic:
by rw [div_eq_mul_inv, inv_zero, mul_zero]

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:
zero_zpow_eq,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ (if n = 0 then 1 else 0) = 1 ↔ n = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
hf : Function.Surjective ⇑f
b : β
x✝ : b ∈ {b | IsSquare b}
r : α
h✝ : b = f r * f r
⊢ b ∈ ⇑f '' {a | IsSquare a}

Tactic:
exact ⟨r * r, by simp [*]⟩

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
⊢ a ↔ a

pp: case head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

pp: case tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

pp: case tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q

Tactic:
· rfl

Goal state after:
case head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

case tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

case tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = d * (b * d⁻¹) * c ↔ d * a = b * c

Tactic:
hbd.symm.left_comm,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = b * (d * d⁻¹) * c ↔ d * a = b * c
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]

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
n : ℕ
x : R
y : M
⊢ (n • x) • y = n • x • y

Tactic:
by
    induction n with
    | zero => simp only [zero_smul]
    | succ n ih => simp only [add_smul, one_smul, ih]

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

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
· rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
    exact h a⁻¹ bc

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
neg_mul_neg

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

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

Tactic:
← mul_le_mul_iff_right b

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a⁻¹ * b ≤ a * b⁻¹ * b ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a < c / b ↔ a * b < c

Tactic:
rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a b : M₀
inst✝ : MulPosMono M₀
ha : a ≤ 1
hb₀ : 0 ≤ b
hb : b ≤ 1
⊢ 1 * b ≤ 1

Tactic:
rwa [one_mul]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : LinearOrder R
b c : R
inst✝ : PosMulStrictMono R
h : 0 < c
⊢ 0 ≤ c * b ↔ 0 ≤ b

Tactic:
by
  convert! mul_le_mul_iff_right₀ h
  simp

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 : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ (n + 1) ≤ a ^ n

Tactic:
zpow_add_one₀ ha₀.ne'

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ n * a ≤ a ^ n
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n

Tactic:
zpow_add_one₀ ha₀.ne'

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n
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 : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ 1 * b

Tactic:
rwa [one_mul]

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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a

Tactic:
subst h

Goal state after:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b : β
a : α
H : ∀ (y : β), s y (f a) → Acc s y
IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a
⊢ Acc r a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosMono G₀
n : ℕ
x✝ : ↑(n + 1) ≠ 0
⊢ Set.InjOn (fun a ↦ a ^ ↑(n + 1)) {a | 0 ≤ a}

Tactic:
by simpa using! mod_cast (pow_left_strictMonoOn₀ n.succ_ne_zero).injOn

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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a

Tactic:
subst h

Goal state after:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b : β
a : α
H : ∀ (y : β), s y (f a) → Acc s y
IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a
⊢ Acc r a