mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous
    (⇑(hom (c.π.app i)) ∘ (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun)

Tactic:
change Continuous (X := s.pt) (Y := F.obj i)
      (hc.lift ((forget₂ _ (ModuleCat R)).mapCone s) ≫ c.π.app i).hom

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s) ≫ c.π.app i))
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
X : C
inst✝ : IsFinitelyPresentable X
⊢ PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (coyoneda.obj (op X))

Tactic:
rw [← isFinitelyPresentable_iff_preservesFilteredColimitsOfSize]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.Ring.LinearAlgebra

Goal state before:
pp: A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
⊢ Nontrivial ↑D

Tactic:
algebraize [f.hom, g.hom]

Goal state after:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
⊢ Nontrivial ↑D
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * y) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) y

pp: case add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝ * y) = (piRightHom R S A B) x✝ * (piRightHom R S A B) y
a✝ : (piRightHom R S A B) (y✝ * y) = (piRightHom R S A B) y✝ * (piRightHom R S A B) y
⊢ (piRightHom R S A B) ((x✝ + y✝) * y) = (piRightHom R S A B) (x✝ + y✝) * (piRightHom R S A B) y

Tactic:
· induction y
    · simp
    · ext j
      simp
    · simp_all [mul_add]

Goal state after:
case add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝ * y) = (piRightHom R S A B) x✝ * (piRightHom R S A B) y
a✝ : (piRightHom R S A B) (y✝ * y) = (piRightHom R S A B) y✝ * (piRightHom R S A B) y
⊢ (piRightHom R S A B) ((x✝ + y✝) * y) = (piRightHom R S A B) (x✝ + y✝) * (piRightHom R S A B) y
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝ : P.ContainsIdentities
Y : P.Under ⊤ X
a : Under.mk ⊤ (𝟙 X) ⋯ ⟶ Y
⊢ a.right = (Under.homMk Y.hom ⋯ ⋯).right

Tactic:
simp [← Under.w a]

Goal state after:
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hR : ExpChar R q
⊢ ExpChar A q

Tactic:
rcases hR with _ | hprime

Goal state after:
case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
⊢ ExpChar A 1

case prime
R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hprime : Nat.Prime q
hchar✝ : CharP R q
⊢ ExpChar A q
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
⊢ tensorKerInv S M f ∘ₗ tensorKer S M f = id

Tactic:
ext m x

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
m : M
x : ↥f.ker
⊢ ((AlgebraTensorModule.curry (tensorKerInv S M f ∘ₗ tensorKer S M f)) m) x = ((AlgebraTensorModule.curry id) m) x
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
⊢ tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g = id

Tactic:
ext m x

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
m : M
x : ↥(f.eqLocus g)
⊢ ((AlgebraTensorModule.curry (tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g)) m) x =
    ((AlgebraTensorModule.curry id) m) x
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
q : ℕ
q_prime : Nat.Prime q
⊢ MixedCharZero R q → P

Tactic:
q_mixedChar

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
q : ℕ
q_prime : Nat.Prime q
q_mixedChar : MixedCharZero R q
⊢ P
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
⊢ MixedCharZero R q → P

Tactic:
q_mixedChar

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
⊢ P
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ (Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0

Tactic:
refine Ideal.Quotient.eq.trans (?_ : ↑x - 0 ∈ I ↔ _)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x - 0 ∈ I ↔ ↑x = 0
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Tactic:
let t := tail s₁ ⋈ tail s₂

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).tail = s₂ ⋈ s₁.tail

Tactic:
unfold interleave corecOn; rw [corec_eq]; rfl

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

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ take n (x ++ₛ a) = List.take n x

Tactic:
apply List.ext_getElem (by simp [h])

Goal state after:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ ∀ (i : ℕ) (h₁ : i < (take n (x ++ₛ a)).length) (h₂ : i < (List.take n x).length),
    (take n (x ++ₛ a))[i] = (List.take n x)[i]
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈ take (l + 1) s

Tactic:
take,

Goal state after:
case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈
    match s.destruct with
    | none => []
    | some (x, r) => x :: take l r
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x ∈ take (k + 1 + l + 1) s

Tactic:
take,

Goal state after:
case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x ∈
    match s.destruct with
    | none => []
    | some (x, r) => x :: take (k + 1 + l) r
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (take n s).length ≤ n

Tactic:
induction n generalizing s with
  | zero => simp
  | succ m ih =>
    rw [take]
    cases s.destruct with
    | none => simp
    | some v =>
      obtain ⟨x, r⟩ := v
      simpa using ih

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ (take (n + 1) s).length = n + 1

Tactic:
take,

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take n r).length =
    n + 1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a' ∈ t

Tactic:
mem_unique ma h1

Goal state after:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (of v).s.get? 0 = (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
by
  rw [of, IntFractPair.seq1]
  simp only [Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.get?, Stream'.map]
  rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]
  split <;> simp_all only [Option.bind_some, Option.bind_none, Function.comp_apply]

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

Goal state before:
pp: m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) = (fib m).gcd (fib (n.pred + 1) * fib (m + 1))

Tactic:
rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
simpa only [convs'Aux, s_head_eq]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n

Tactic:
exact IntFractPair.coe_stream_nth_rat_eq v_eq_q n

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ x ∈ P.toPoly.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
mem_roots h0,

Goal state after:
R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ P.toPoly.IsRoot x ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
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
ha : P.a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3

Tactic:
replace ha : (map φ P).a ≠ 0 := (map_ne_zero φ).mpr ha

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3
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
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : (Polynomial.map φ P.toPoly).Splits
hd : P.discr ≠ 0
⊢ (map φ P).roots.toFinset.card = 3

Tactic:
rwa [toFinset_card_of_nodup <| (discr_ne_zero_iff_roots_nodup ha h3).mp hd,
    ← splits_iff_card_roots ha]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
⊢ e₁ = e₂

Tactic:
rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) k ≠ ⊥
⊢ (f.genEigenspace μ) m ≠ ⊥

Tactic:
contrapose hk

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k = ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
hμp : Disjoint (f.eigenspace μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ = ⊥

Tactic:
by
  rw [eq_bot_iff]
  intro x hx
  simpa using hμp.le_bot ⟨eigenspace_restrict_le_eigenspace f hfp μ ⟨x, hx, rfl⟩, x.prop⟩

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
inj : Injective ⇑(f 0)
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
surj : Surjective ⇑(f (Fin.last n))
⊢ ∑ i, (-1) ^ ↑i * ↑(finrank k (V i)) = 0

Tactic:
replace inj := LinearMap.finrank_range_of_inj inj
  replace surj := LinearMap.range_eq_top.mpr surj
  simp_rw [← smul_eq_mul]
  refine Fin.sum_neg_one_pow_eq_zero _ (fun i ↦ finrank k (f i).range) ?_ (fun i ↦ ?_) ?_
  · aesop
  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
      ```
      grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
      ```
      -/
    have hrn := (f i.succ).finrank_range_add_finrank_ker
    have hker : finrank k ↥(LinearMap.ker (f i.succ)) =
        finrank k ↥(LinearMap.range (f i.castSucc)) :=
      congrArg (fun S : Submodule k (V i.succ.castSucc) => finrank k ↥S)
        (h_exact i).linearMap_ker_eq
    omega
  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
      ```
      grind [finrank_top]
      ```
      -/
    rw [surj, finrank_top, Fin.succ_last]

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

Tactic:
apply e.injective.field _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
by
  have hX := mk_freeMonoid X
  rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq,
    MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite, hX, lift_max, lift_aleph0, sup_assoc]

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

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
⊢ IsIntegrallyClosed R

Tactic:
let f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom (g := Algebra.ofId _ _)
    (FaithfulSMul.algebraMap_injective R K)

Goal state after:
R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
⊢ IsIntegrallyClosed R
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ ∃ a b, IsUnit (gcd a b) ∧ mk' A x ⟨y, hy⟩ * (algebraMap R A) b = (algebraMap R A) a

Tactic:
use x', y', hu

Goal state after:
case right
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A x ⟨y, hy⟩ * (algebraMap R A) y' = (algebraMap R A) x'
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: ι : 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✝¹ : SMul M N
inst✝ : ∀ (i : ι), IsScalarTower M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ (a • b) • x = a • b • x

Tactic:
cases x
    rw [smul_mk, smul_mk, smul_mk, smul_assoc]

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

Goal state before:
pp: case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = ((-1) ^ (n - k) * ↑(n.choose k)) • (shiftₗ M G h ^ k) f y

Tactic:
shiftₗ_pow_apply

Goal state after:
case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝ : DivInvMonoid M
s t : Set M
⊢ #↑(s / t) ≤ #↑s * #↑t

Tactic:
by
  rw [← image2_div]; exact Cardinal.mk_image2_le

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure s

Tactic:
← Subtype.range_coe (s := s)

Goal state after:
M : Type u_1
inst✝¹ : CommGroup M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure (Set.range Subtype.val)
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : comap φ M ≠ comap φ ⊤
⊢ comap φ M ≠ ⊤

Tactic:
comap_top

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : comap φ M ≠ ⊤
⊢ comap φ M ≠ ⊤
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < K → K = comap φ ⊤
hK : comap φ M < K
⊢ K = ⊤

Tactic:
comap_top

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < K → K = ⊤
hK : comap φ M < K
⊢ K = ⊤
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure s

Tactic:
← Subtype.range_coe (s := s)

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure (Set.range Subtype.val)
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsReduced M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
⊢ IsMulTorsionFree M

Tactic:
by
  refine ⟨fun n hn x y hxy ↦ ?_⟩
  by_cases h : x ≠ 0 ∧ y ≠ 0
  · exact ih x h.1 y h.2 n hn hxy
  grind [eq_zero_of_pow_eq_zero, zero_pow]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rcases le_or_gt i k with (hik | hik)

Goal state after:
case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ rev.map (δ i) = δ i.rev

Tactic:
by
  ext j : 3
  simp [δ, Fin.succAbove_rev_right, Fin.rev_rev, rev_map_apply]

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

Goal state before:
pp: X : SSet
n k : ℕ
hk : n ≤ k
⊢ ⊥.toSSet.degenerate k = ⊤

Tactic:
by
    ext ⟨x, hx⟩
    tauto

Goal state after: