mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_num_eq : g.nums n = ppredA
succ_nth_num_eq : g.nums (n + 1) = predA
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredA

Tactic:
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.a = ppredA :=
    exists_conts_a_of_num nth_num_eq
  obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
      ∃ conts, g.conts (n + 1) = conts ∧ conts.a = predA :=
    exists_conts_a_of_num succ_nth_num_eq
  rw [num_eq_conts_a, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : DirectLimit G f
⊢ ∃ i x, (of G f i) x = z

Tactic:
obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective z
  refine z.induction_on ⟨Classical.arbitrary ι, -1, by simp; rfl⟩ (fun ⟨i, x⟩ ↦ ⟨i, x, rfl⟩) ?_ ?_
    <;> rintro x' y' ⟨i, x, hx⟩ ⟨j, y, hy⟩ <;> have ⟨k, hik, hjk⟩ := exists_ge_ge i j
  · exact ⟨k, f i k hik x + f j k hjk y, by rw [map_add, of_f, of_f, hx, hy]; rfl⟩
  · exact ⟨k, f i k hik x * f j k hjk y, by rw [map_mul, of_f, of_f, hx, hy]; rfl⟩

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ C ((of G (fun i j h ↦ ⇑(f' i j h)) i) x) = C z

Tactic:
h

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ C z = C z
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)

Tactic:
intro _ h3 _ h1
    rw [think_bind]
    obtain ⟨m', h⟩ := of_results_think h1
    obtain ⟨h1, e⟩ := h
    rw [e]
    exact results_think (h3 h1)

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' s : Computation α
⊢ (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s' s → BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct

Tactic:
h

Goal state after:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' s : Computation α
⊢ (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s' s → BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct

Tactic:
h

Goal state after:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x1 x2 ↦ x1 = x2) (map f s1) (map f s2)

Tactic:
exact liftRel_map Eq _ ((lift_eq_iff_equiv _ _).2 h1) fun {a} b => congr_arg _

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
⊢ (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1 s2 →
    BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1.destruct
      s2.destruct

Tactic:
h

Goal state after:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1.destruct
    s2.destruct
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ convs'Aux (of v).s (n + 1) = 1 / (of (fract v)⁻¹).convs' n

Tactic:
convs'Aux_succ_some (of_s_head h)

Goal state after:
case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.a / ({ a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n) =
    1 / (of (fract v)⁻¹).convs' n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : s.TerminatedAt n
⊢ p y

Tactic:
simp [get?_set_of_terminatedAt _ h_term] at hy

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

Goal state before:
pp: n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
zify [this]

Goal state after:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ ↑(fib n) * (2 * ↑(fib (n + 1)) - ↑(fib n)) + (↑(fib (n + 1)) ^ 2 + ↑(fib n) ^ 2) =
    ↑(fib (n + 1)) * (2 * ↑(fib n) + ↑(fib (n + 1)))
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ (C P.b * X ^ 2 + C P.c * X + C P.d).degree = 2

Tactic:
degree_quadratic hb

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ 2 = 2
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * ((X - C x) * ((X - C y) * {X - C z}.prod)) = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Tactic:
prod_singleton,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * ((X - C x) * ((X - C y) * (X - C z))) = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
this : |(-1) ^ n / den'| ≤ 1 / den
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)

Tactic:
by grind [sub_convs_eq]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ P.discr ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
by
  rw [← map_ne_zero φ, discr_eq_prod_three_roots ha h3, pow_two]
  simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * (g * h)) = (trace R M) (h * (f * g))

Tactic:
rw [← mul_assoc, LinearMap.trace_mul_comm]

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
⊢ DivisionRing α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
⊢ DivisionRing α
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : 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
⊢ Field α

Tactic:
let mul := e.mul

Goal state after:
α : 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
⊢ Field α
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> traverse g (x * y))

Tactic:
traverse_mul

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g x <*> traverse g y))
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (Polynomial.map (algebraMap R S) f).IsRoot x
hmo : f.Monic
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
exact pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R ≃+* S
h : IsIntegrallyClosed R
⊢ IsIntegrallyClosed S

Tactic:
let _ : Algebra S R := f.symm.toRingHom.toAlgebra
  let f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv fun _ ↦ rfl
  let g : FractionRing S ≃ₐ[S] FractionRing R := IsFractionRing.algEquivOfAlgEquiv f
  refine (isIntegrallyClosed_iff (FractionRing S)).mpr (fun hx ↦ ?_)
  rcases (isIntegrallyClosed_iff _).mp h ((isIntegral_algEquiv g).mpr hx).tower_top with ⟨z, hz⟩
  exact ⟨f.symm z, (IsFractionRing.algEquivOfAlgEquiv_algebraMap f.symm z).symm.trans <|
    (AlgEquiv.symm_apply_eq g).mpr hz⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
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
⊢ q ∣ C g.leadingCoeff * q ^ m * (C h.leadingCoeff * q ^ n)

Tactic:
exact ((dvd_pow_self q hn).mul_left _).mul_left _

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: n : ℕ
m : ℤ
⊢ m ∈ (nsmulAddMonoidHom n).range ↔ m ∈ zmultiples ↑n

Tactic:
simp [mem_zmultiples_iff, dvd_def]

Goal state after:
n : ℕ
m : ℤ
⊢ (∃ x, ↑n * x = m) ↔ ∃ c, m = ↑n * c
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

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

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]
  -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
  · ext; simp only [mem_inv', ne_eq, not_false_eq_true, ← inv_smul_mem_iff₀, smul_eq_mul,
      MulOpposite.op_inv, inv_eq_zero, MulOpposite.op_eq_zero_iff, inv_inv,
      MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_rev, ha]

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
⊢ SemigroupWithZero α

Tactic:
let mul := e.mul

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
⊢ MulZeroClass α

Tactic:
let mul := e.mul

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
⊢ MulZeroOneClass α

Tactic:
let mul := e.mul

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
⊢ MonoidWithZero α

Tactic:
let _ := e.mulZeroOneClass

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝ : MulZeroOneClass α := e.mulZeroOneClass
⊢ MonoidWithZero α
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : x ^ n = (x * ↑u) ^ n
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
mul_pow,

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : x ^ n = x ^ n * ↑u ^ n
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_1.mem
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y x✝ : Bˣ
a : A
ha : f a = ↑x✝
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑x✝ = f x

Tactic:
exact ⟨a, ha.symm ▸ Units.ne_zero _, ⟨a * a, by simp [← ha]⟩⟩

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
⊢ (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂ → a₁ = a₂

Tactic:
h

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
⊢ a₁ = a₂
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: a b : SimplexCategory
f g : a ⟶ b
h : f = g
x : Fin (a.len + 1)
⊢ (Hom.toOrderHom f) x = (Hom.toOrderHom g) x

Tactic:
h

Goal state after:
a b : SimplexCategory
f g : a ⟶ b
h : f = g
x : Fin (a.len + 1)
⊢ (Hom.toOrderHom g) x = (Hom.toOrderHom g) x
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f

Tactic:
h

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ g.f = g.f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ δ i ≫ δ j = δ i ≫ δ i.succ

Tactic:
subst H

Goal state after:
n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ i.castSucc = δ i ≫ δ i.succ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
subst H

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
subst H

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = i.castSucc
⊢ X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
subst H

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)

Tactic:
subst H

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)

Tactic:
subst H

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n m : ℕ
h : n = m
⊢ ⦋n⦌ = ⦋m⦌

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n m : ℕ
h : n = m
⊢ ⦋m⦌ = ⦋m⦌
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ X.δ i ≫ X.δ j = X.δ i ≫ X.δ i.succ

Tactic:
subst H

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
subst H

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
subst H

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
⊢ i ≤ j → f.symm i ≤ f.symm j

Tactic:
h

Goal state after:
X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
h : i ≤ j
⊢ f.symm i ≤ f.symm j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
h : i ≤ j
⊢ (Finset.univ.orderEmbOfFin aux) (f.symm i) ≤ (Finset.univ.orderEmbOfFin aux) (f.symm j)

Tactic:
change f (f.symm i) ≤ f (f.symm j)

Goal state after:
X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
h : i ≤ j
⊢ f (f.symm i) ≤ f (f.symm j)
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : X ⟶ F.augmentedCechNerve
⊢ (𝟭 C).map (G.left.app (Opposite.op ⦋0⦌) ≫ WidePullback.π (fun x ↦ F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right

Tactic:
have := G.w
    apply_fun fun e => e.app (Opposite.op ⦋0⦌) at this
    simpa using this

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s t : X.S
⊢ s ≤ t ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex

Tactic:
rw [le_def, Subcomplex.ofSimplex_le_iff, Subfunctor.ofSection_obj, Set.mem_ofPred_eq]

Goal state after:
X : SSet
s t : X.S
⊢ (∃ f, (ConcreteCategory.hom (X.map f)) t.simplex = s.simplex) ↔
    ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ range f = ⊤ ↔ Epi f

Tactic:
rw [NatTrans.epi_iff_epi_app, Subfunctor.ext_iff, funext_iff]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ (∀ (x : SimplexCategoryᵒᵖ), (range f).obj x = ⊤.obj x) ↔ ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case inr
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
d' : ℕ
y : X _⦋d'⦌
hy : y ∈ X.nonDegenerate d'
h : mk ↑⟨x, hx⟩ ⋯ < mk ↑⟨y, hy⟩ ⋯
h' : (mk ↑⟨x, hx⟩ ⋯).dim = (mk ↑⟨y, hy⟩ ⋯).dim
f : ⦋(mk ↑⟨x, hx⟩ ⋯).dim⦌ ⟶ ⦋(mk ↑⟨y, hy⟩ ⋯).dim⦌
w✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (mk ↑⟨y, hy⟩ ⋯).simplex = (mk ↑⟨x, hx⟩ ⋯).simplex
⊢ (mk ↑⟨x, hx⟩ ⋯).dim < (mk ↑⟨y, hy⟩ ⋯).dim

Tactic:
obtain rfl : d = d' := h'

Goal state after:
case inr
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h : mk ↑⟨x, hx⟩ ⋯ < mk ↑⟨y, hy⟩ ⋯
f : ⦋(mk ↑⟨x, hx⟩ ⋯).dim⦌ ⟶ ⦋(mk ↑⟨y, hy⟩ ⋯).dim⦌
w✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (mk ↑⟨y, hy⟩ ⋯).simplex = (mk ↑⟨x, hx⟩ ⋯).simplex
⊢ (mk ↑⟨x, hx⟩ ⋯).dim < (mk ↑⟨y, hy⟩ ⋯).dim