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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
⊢ (a * if h : P then b h else c h) = if h : P then a * b h else a * c h

Tactic:
by split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Tactic:
by split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h

Tactic:
by split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Tactic:
by split <;> rfl

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

Goal state before:
pp: α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
⊢ (-if P then b else c) = if P then -b else -c

Tactic:
by split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Tactic:
by split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Tactic:
by split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h

Tactic:
by split <;> rfl

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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ y * (a * x') = y * y' * a

Tactic:
h'.eq,

Goal state after:
S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ y * (y' * a) = y * y' * a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
· exact h₁

Goal state after:
case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c
Module: Mathlib.Logic.Unique

Goal state before:
pp: A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f

Tactic:
rw [Function.bijective_iff_has_inverse]
  refine ⟨default, ?_, ?_⟩ <;> intro x <;> simp

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

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False

Tactic:
let T : Type max u v := Sigma f

Goal state after:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ r ≤ (Relation.Map r f f on f)

Tactic:
by
  unfold Pi.hasLe Prop.le
  grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ Relation.Map (r on f) f f ≤ r

Tactic:
by
  unfold Pi.hasLe Prop.le
  grind [Relation.Map]

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✝ : IsTrans α r
a b : α
h₁ : ReflGen r a b
⊢ ReflGen r a b

pp: case 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₁ : ReflGen r a b
h₂ : r b c
⊢ ReflGen r a c

Tactic:
· exact h₁

Goal state after:
case 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₁ : ReflGen r a b
h₂ : r b c
⊢ ReflGen r a c
Module: Mathlib.Logic.Relation

Goal state before:
pp: case 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✝ : Std.Symm r
x y b✝ : α
i : r x b✝
⊢ TransGen r b✝ x

Tactic:
exact .single <| symm i

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
induction h with
      | refl => exact refl a
      | tail _ h₂ IH => exact IsTrans.trans _ _ _ IH h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ f' (gb x) = ga (f' x)

Tactic:
by
  rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]

Goal state after:
Module: Mathlib.Logic.Pairwise

Goal state before:
pp: n : ℕ
R : Fin n.succ → Fin n.succ → Prop
inst✝ : Std.Symm R
⊢ Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun i j ↦ R i.succ j.succ

Tactic:
simp only [pairwise_fin_succ_iff, comm (b := 0) (r := R), and_self_left]

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

Goal state before:
pp: α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Bijective (rangeFactorization f) ↔ Function.Injective f

Tactic:
simp [Function.Bijective]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (Monotone fun x ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g

Tactic:
simp_rw [Monotone, Prod.mk_le_mk, forall_and]

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
exact h_mon h₁

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ a ≤ a ⊔ b

Tactic:
by
    rw [← le, map_sup]
    exact le_sup_left

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
⊢ (a ≤ if b ≤ c then ⊤ else c) ↔ min a b ≤ c

Tactic:
split_ifs with h
      · exact iff_of_true le_top (inf_le_of_right_le h)
      · rw [inf_le_iff, or_iff_left h]

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

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

pp: case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
· rw [removeNoneAux_none _ h2] at h1
        simp at h1

Goal state after:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
a : α
⊢ (fun b ↦ ((↑e).symm ↑b).get ⋯) ((fun a ↦ ⟨↑e (some a), ⋯⟩) a) = a

Tactic:
rw [← some_inj, some_get]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
a : α
⊢ (↑e).symm ↑((fun a ↦ ⟨↑e (some a), ⋯⟩) a) = some a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hxz : x ≤ z
hyz : y ≤ z
h : z \ x = z \ y
⊢ z \ (z \ y) = y

Tactic:
sdiff_sdiff_eq_self hyz

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hxz : x ≤ z
hyz : y ≤ z
h : z \ x = z \ y
⊢ y = y
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
⊢ subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε

Tactic:
ext x
  by_cases h : p x <;> simp [h]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sup_idem,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a \ a = ⊥
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π i

Tactic:
by rw [← f.2 i]; exact (f.1 i).2

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff_sdiff]
  simp [symmDiff]

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
β : α → Sort v
p : (a : α) → β a → Prop
⊢ RightInverse (fun f ↦ ⟨fun a ↦ ↑(f a), ⋯⟩) fun f a ↦ ⟨↑f a, ⋯⟩

Tactic:
rintro f

Goal state after:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → { b // p a b }
⊢ (fun f a ↦ ⟨↑f a, ⋯⟩) ((fun f ↦ ⟨fun a ↦ ↑(f a), ⋯⟩) f) = f
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ t ⊆ f '' s ↔ ∃ u, u ⊆ s ∧ f '' u = t

Tactic:
refine ⟨fun h ↦ ⟨f ⁻¹' t ∩ s, inter_subset_right, ?_⟩,
    fun ⟨u, hu, hu'⟩ ↦ hu'.symm ▸ image_mono hu⟩
  rwa [image_preimage_inter, inter_eq_left]

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

Goal state before:
pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
by_cases h' : i ∈ s

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : ¬i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

Tactic:
apply piecewise_le <;> intros <;> simp [*]

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) <;> simp [*, forall_and, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g '' f '' s = s

Tactic:
rw [← image_comp, h.comp_eq_id, image_id]

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
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
rw [Set.ext_iff] at he₁ 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₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ
e₂ : γ → β
he₂ : ∀ (x : γ × β), x ∈ range (⇑(Equiv.prodComm β γ) ∘ f) ↔ x ∈ graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: β : Type u_2
γ : Type u_3
s : Set (β × γ)
hs₁ : Bijective (Prod.fst ∘ Subtype.val)
⊢ ∃ f, s = graphOn f univ

Tactic:
by
  simpa using exists_range_eq_graphOn_univ hs₁.surjective
    fun a b h ↦ congr_arg (Prod.snd ∘ (Subtype.val : s → β × γ)) (hs₁.injective h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
⊢ f (f' y) = y

Tactic:
rw [← heq, hf' hx]

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ Int.leInductionDown base pred (n - 1) ⋯ = pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
by
  rw [Int.leInductionDown, inductionOn'_sub_one hnm]
  rfl

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

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

Tactic:
by rw [Nat.mod_add_div]

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

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

Tactic:
← inv_div,

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

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

Tactic:
← inv_div,

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
u : Mˣ
⊢ IsUnit (↑u ^ n)

Tactic:
exact ⟨u ^ n, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
c : α
h : IsUnit c
a b : α
⊢ a * c / (b * c) = a / b

Tactic:
by
  simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsLeftCancelMulZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsLeftCancelMulZero M₀
a b c : M₀
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

case neg
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsLeftCancelMulZero M₀
a b c : M₀
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case neg
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsRightCancelMulZero M₀
a b c : M₀
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
simp [mul_left_inj', hc]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap ((swap y z) x) z = swap z x

Tactic:
swap_apply_of_ne_of_ne hxy hxz,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap x z = swap z x
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
by_cases ha : a = 0

Goal state after:
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⁻¹

case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : ¬a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : ¬a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
· exact zpow_add₀ ha m n

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

Goal state before:
pp: n : ℤ
⊢ ↑(n * n).toNat.sqrt = ↑n.natAbs

Tactic:
← natAbs_mul_self,

Goal state after:
n : ℤ
⊢ ↑(↑(n.natAbs * n.natAbs)).toNat.sqrt = ↑n.natAbs
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
b c a : α
h : b ∣ c
⊢ a * b ∣ a * c

Tactic:
by
  obtain ⟨d, rfl⟩ := h
  use d
  rw [mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
b c a : α
h : b ∣ᵣ c
⊢ b * a ∣ᵣ c * a

Tactic:
by
  obtain ⟨d, rfl⟩ := h
  use d
  rw [mul_assoc]

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

Goal state before:
pp: case succ
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
· exact h_pos n.succ_pos

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 * (1 / -a) = b * -(1 / a)

Tactic:
rw [one_div_neg_eq_neg_one_div]

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(ofNat a✝) = 0
⊢ ofNat a✝ = 0

pp: case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0

Tactic:
· rw [ofNat_eq_natCast, Int.cast_natCast] at h
      exact congr_arg _ (Nat.cast_eq_zero.1 h)

Goal state after:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0
Module: Mathlib.Data.Int.Cast.Lemmas

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

Tactic:
simp [zsmul_add]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective 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
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (x * -y) = f (-(x * y))

Tactic:
by rw [neg, mul, neg, mul_neg, mul]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ (n + 1))

Tactic:
rw [pow_succ]; exact ha.mul_left _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ |a⁻¹|ₘ = |a|ₘ

Tactic:
simp [mabs, sup_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a * b|ₘ ≤ |a|ₘ * |b|ₘ

Tactic:
by
  apply sup_le
  · exact mul_le_mul' (le_mabs_self a) (le_mabs_self b)
  · rw [mul_inv]
    exact mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ⊔ b / a ⊔ 1 = |b / a|ₘ

Tactic:
← inv_div,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (b / a)⁻¹ ⊔ b / a ⊔ 1 = |b / a|ₘ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, (x.xgcdAux 1 0 y 0 1).2)

Tactic:
← xgcdAux_fst x y 1 0 0 1

Goal state after:
x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = ((x.xgcdAux 1 0 y 0 1).1, (x.xgcdAux 1 0 y 0 1).2)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
· rcases le_total a c with hc | hc
    · simp [hc, le_mul_left]
    · simp [hb, hc]

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑q * ↑p.succ + -1 * ↑q.succ = ↑p * ↑q - 1

Tactic:
by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia

Goal state after: