mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case qsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ) (x : α), e (q • x) = q • e x

Tactic:
intros

Goal state after:
case qsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ
x✝ : α
⊢ e (q✝ • x✝) = q✝ • e x✝
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
intros

Goal state after:
case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case zpow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n

Tactic:
intros

Goal state after:
case zpow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℤ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℤ
⊢ e ↑n✝ = ↑n✝
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case nnratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ≥0), e ↑q = ↑q

Tactic:
intros

Goal state after:
case nnratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ≥0
⊢ e ↑q✝ = ↑q✝
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case ratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ), e ↑q = ↑q

Tactic:
intros

Goal state after:
case ratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ
⊢ e ↑q✝ = ↑q✝
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x : FreeMagma α
⊢ ∀ (x y : FreeMagma α), f x = g x → f y = g y → f (x * y) = g (x * y)

Tactic:
intros

Goal state after:
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case zero
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0

Tactic:
intros

Goal state after:
case zero
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case add
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x y : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (x + y) = (equivProd c₁ c₂ c₃) x + (equivProd c₁ c₂ c₃) y

Tactic:
intros

Goal state after:
case add
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ + y✝) = (equivProd c₁ c₂ c₃) x✝ + (equivProd c₁ c₂ c₃) y✝
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case neg
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (-x) = -(equivProd c₁ c₂ c₃) x

Tactic:
intros

Goal state after:
case neg
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (-x✝) = -(equivProd c₁ c₂ c₃) x✝
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case sub
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x y : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (x - y) = (equivProd c₁ c₂ c₃) x - (equivProd c₁ c₂ c₃) y

Tactic:
intros

Goal state after:
case sub
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ - y✝) = (equivProd c₁ c₂ c₃) x✝ - (equivProd c₁ c₂ c₃) y✝
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case nsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℕ), (equivProd c₁ c₂ c₃) (n • x) = n • (equivProd c₁ c₂ c₃) x

Tactic:
intros

Goal state after:
case nsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℕ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case zsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℤ), (equivProd c₁ c₂ c₃) (n • x) = n • (equivProd c₁ c₂ c₃) x

Tactic:
intros

Goal state after:
case zsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℤ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ (Ideal.Quotient.mk (P ^ 2)) (r.coeff x.1 * s.coeff x.2) = 0

Tactic:
rw [eq_zero_iff_mem, pow_two]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ r.coeff x.1 * s.coeff x.2 ∈ P * P
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ x ∣ y ^ p.natDegree

Tactic:
by
  rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]
  refine
    (scaleRoots.isWeaklyEisensteinAt _
          (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
      ?_ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl
  rw [injective_iff_map_eq_zero'] at hf
  have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
  rwa [hz, Polynomial.eval₂_at_apply, hf] at this

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

Goal state before:
pp: case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b : α i
x : (i : ι) × α i
inst✝¹ : (i : ι) → SMul Mᵐᵒᵖ (α i)
inst✝ : ∀ (i : ι), IsCentralScalar M (α i)
a : M
fst✝ : ι
snd✝ : α fst✝
⊢ MulOpposite.op a • ⟨fst✝, snd✝⟩ = a • ⟨fst✝, snd✝⟩

Tactic:
rw [smul_mk, smul_mk, op_smul_eq_smul]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ s ⊆ univ * s

Tactic:
exact fun x hx => ⟨1, mem_univ 1, x, hx, by simp⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(closure s) = univ * s

Tactic:
rw [coe_closure, union_eq_right]
  exact fun x hx => ⟨1, mem_univ 1, x, hx, by simp⟩

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
n : ℕ+
⊢ x ^ n = x ^ ↑n

Tactic:
induction n with
  | one => rw [ppow_one, PNat.one_coe, pow_one]
  | succ k hk => rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

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

Goal state before:
pp: M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (m * n) = (x ^ m) ^ n

Tactic:
induction n with
  | zero => rw [npow_zero, mul_zero, npow_zero]
  | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]

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

Goal state before:
pp: M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
x h : M
n : ℕ
⊢ Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x

Tactic:
induction n generalizing x with

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0

Tactic:
intros

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

Tactic:
intros

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ ∀ (a b : α), e (a * b) = e a * e b

Tactic:
intros

Goal state after:
case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

Tactic:
intros

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

Tactic:
intros

Goal state after:
case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ ∀ (a b : α), e (a * b) = e a * e b

Tactic:
intros

Goal state after:
case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0

Tactic:
intros

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1

Tactic:
intros

Goal state after:
case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
intros

Goal state after:
case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 0 = 0

Tactic:
intros

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 1 = 1

Tactic:
intros

Goal state after:
case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 1 = 1
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
intros

Goal state after:
case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow =
    0

Tactic:
rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero,
      ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Abelian D
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
intros

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Abelian D
X✝ : D
p✝ : X✝ ⟶ X✝
a✝ : p✝ ≫ p✝ = p✝
⊢ HasKernel p✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
⊢ (∃ a, f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
by
  match e0 : f.toOrderHom 0, e1 : f.toOrderHom 1 with
  | 0, 0 | 1, 1 =>
    refine .inl ⟨f.toOrderHom 0, ?_⟩
    ext i : 3
    match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
  | 0, 1 =>
    right
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1
  | 1, 0 =>
    have := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)
    rw [e0, e1] at this
    exact Not.elim (by decide) this

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (P.decompId_p ≫ P.decompId_i).f

Tactic:
simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i'

Tactic:
simpa [φ] using! congr_arg Prod.snd h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplicialObject C)

Tactic:
dsimp [SimplicialObject]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplicialObject C)

Tactic:
dsimp [SimplicialObject]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)