mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app (op U)))

Tactic:
by
  refine app_surjective_of_injective_of_locally_surjective f U (And.left <| h · ·) fun t x hx => ?_
  -- Now we need to prove our initial claim: That we can find preimages of `t` locally.
  -- Since `f` is surjective on stalks, we can find a preimage `s₀` of the germ of `t` at `x`
  obtain ⟨s₀, hs₀⟩ := (h x hx).2 (G.presheaf.germ U x hx t)
  -- ... and this preimage must come from some section `s₁` defined on some open neighborhood `V₁`
  obtain ⟨V₁, hxV₁, s₁, rfl⟩ := F.presheaf.exists_germ_eq s₀
  rename' hs₀ => hs₁
  rw [stalkFunctor_map_germ_apply V₁ x hxV₁ f.1 s₁] at hs₁
  -- Now, the germ of `f.app (op V₁) s₁` equals the germ of `t`, hence they must coincide on
  -- some open neighborhood `V₂`.
  obtain ⟨V₂, hxV₂, iV₂V₁, iV₂U, heq⟩ := G.presheaf.germ_eq x hxV₁ hx _ _ hs₁
  -- The restriction of `s₁` to that neighborhood is our desired local preimage.
  use V₂, hxV₂, iV₂U, F.1.map iV₂V₁.op s₁
  rw [← ConcreteCategory.comp_apply, f.1.naturality, ConcreteCategory.comp_apply, heq]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousSMul S B'

Tactic:
apply ContinuousSMul.mk

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := ⋯
hφo : IsOpenQuotientMap ⇑φ
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ) inst✝³] fun p ↦ p.1 • p.2
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
⊢ Function.Injective toLinearMap

Tactic:
by
  intro f g H
  cases f
  cases g
  congr

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ (↑e ∘SL f).IsInvertible ↔ f.IsInvertible

Tactic:
by
  constructor
  · rintro ⟨A, hA⟩
    have : f = e.symm ∘L ((e : M₂ →L[R] M₃) ∘L f) := by ext; simp
    rw [this, ← hA]
    simp
  · rintro ⟨M, rfl⟩
    simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ (↑e ∘SL f).inverse = f.inverse ∘SL ↑e.symm

Tactic:
rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, zero_comp]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f ∘SL f.inverse = ContinuousLinearMap.id R M₂

Tactic:
by
  rcases hf with ⟨e, rfl⟩
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
y : M₂
⊢ f (f.inverse y) = y

Tactic:
by
  rcases hf with ⟨e, rfl⟩
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f.inverse ∘SL f = ContinuousLinearMap.id R M

Tactic:
by
  rcases hf with ⟨e, rfl⟩
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
y : M
⊢ f.inverse (f y) = y

Tactic:
by
  rcases hf with ⟨e, rfl⟩
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f.inverse.IsInvertible

Tactic:
by
  rcases hf with ⟨e, rfl⟩
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f.inverse.inverse = f

Tactic:
by
  rcases hf with ⟨e, rfl⟩
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
⊢ h.coneπApp i₀ = 𝟙 (F.obj i₀)

Tactic:
rw [h.coneπApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_inv_hom_id]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
obtain ⟨κF, _, _⟩ := IsAccessible.exists_cardinal (F := F)
  obtain ⟨κG, _, _⟩ := IsAccessible.exists_cardinal (F := G)
  have : Fact (κF ⊔ κG).IsRegular := ⟨iteInduction (fun _ ↦ Fact.out) (fun _ ↦ Fact.out)⟩
  have := isCardinalAccessible_of_le F (by simp : κF ≤ κF ⊔ κG)
  have := isCardinalAccessible_of_le G (by simp : κG ≤ κF ⊔ κG)
  exact isAccessible_of_isCardinalAccessible (F ⋙ G) (κF ⊔ κG)

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

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
hn : ∃ f_1, Function.Surjective ⇑f_1 ∧ (ker f_1.toRingHom).FG
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
⊢ ∃ π, iP ≫ π = f ∧ Function.Surjective ⇑(ConcreteCategory.hom π) ∧ (ker (CommRingCat.Hom.hom π)).FG

Tactic:
obtain ⟨π, h₁, h₂⟩ := hn
    exact ⟨CommRingCat.ofHom π, by ext1; exact π.comp_algebraMap, h₁, h₂⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app none ≫ Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app none

Tactic:
simp [← Under.comp_right]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case some.left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.left) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.left)

Tactic:
simp [← Under.comp_right]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case some.right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.right) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.right)

Tactic:
simp [← Under.comp_right]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
hp : Nat.Prime p
n : ℕ
⊢ IsUnit ↑(-↑n) ↔ ¬↑p ∣ -↑n

Tactic:
· simp [CharP.isUnit_natCast_iff hp, Int.dvd_neg, Int.ofNat_dvd]

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

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)

Tactic:
rw [← Stream'.eta (iterate f a)]
  rw [tail_iterate]; rfl

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

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
⊢ ¬s.get? n = none

Tactic:
hn

Goal state after:
case refine_1
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
hn : s.get? n = none
⊢ False
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.partNums.get? n = none ↔ g.s.get? n = none

Tactic:
cases s_nth_eq : g.s.get? n <;> simp [partNums, s_nth_eq]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
a : α
as : a ∈ s
fb : b ∈ (pure ∘ f) a
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
exact ⟨a, as, mem_unique (ret_mem _) fb⟩

Goal state after:
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
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (of v).s.get? n = some { a := 1, b := ↑ifp_succ_n.b }

Tactic:
unfold of IntFractPair.seq1

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      n =
    some { a := 1, b := ↑ifp_succ_n.b }
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n

Tactic:
cases n <;> simp

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ p * inv G f p = 1

Tactic:
inv,

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ (p * if H : p = 0 then 0 else Classical.choose ⋯) = 1
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ 0 → g.contsAux m = (g.squashGCF 0).contsAux m
m_le_n : m' + 1 ≤ 0
⊢ g.contsAux (m' + 1) = (g.squashGCF 0).contsAux (m' + 1)

Tactic:
exact (m'.not_succ_le_zero m_le_n).elim

Goal state after:
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)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ 1 / den' ≤ 1 / den

Tactic:
suffices 0 < den ∧ den ≤ den' from div_le_div_of_nonneg_left zero_le_one this.1 this.2

Goal state after:
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)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ 0 < den ∧ den ≤ den'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : Option I
ne : i ≠ j
⊢ (fun x1 x2 ↦ x1.elim x e * x2.elim x e = 0) i j

Tactic:
rcases i with - | i <;> rcases j with - | j
    · cases ne rfl
    · simpa only [mul_assoc, Finset.sum_mul, he.mul_eq, Finset.sum_ite_eq', Finset.mem_univ,
        ↓reduceIte, zero_mul] using! congr_arg (· * e j) hx₁
    · simpa only [Option.elim_some, Option.elim_none, ← mul_assoc, Finset.mul_sum, he.mul_eq,
        Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, mul_zero] using! congr_arg (e i * ·) hx₂
    · exact he.ortho (Option.some_inj.ne.mp ne)

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

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
⊢ finrank K V ≤ n →
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) =
      ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

Tactic:
hn

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) =
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V)

Tactic:
change (f.genEigenspace μ) n ≤ (f.genEigenspace μ) (finrank K V)

Goal state after:
case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ (f.genEigenspace μ) ↑n ≤ (f.genEigenspace μ) ↑(finrank K V)
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
this : f ↑((b i) k) = 0
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

Tactic:
by simp [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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : ¬(μ₁ = μ₂ ∨ μ₁ ∈ s)
⊢ ?m.80

Tactic:
not_or

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : ¬μ₁ = μ₂ ∧ μ₁ ∉ s
⊢ ?m.80
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
by
  let W₀ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₀
  let W₁ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₁
  let W₂ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₂
  let W₃ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₃
  let W₄ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₄
  let W₅ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₅
  let g₀ : W₀ →ₗ[k] W₁ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₀ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₁ : W₁ →ₗ[k] W₂ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₁ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₂ : W₂ →ₗ[k] W₃ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₂ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₃ : W₃ →ₗ[k] W₄ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₃ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₄ : W₄ →ₗ[k] W₅ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₄ ∘ₗ ULift.moduleEquiv.toLinearMap
  have := sum_neg_one_pow_finrank_eq_zero_of_exact_six_aux g₀ g₁ g₂ g₃ g₄
    (inj := by simpa [g₀]) (surj := by simpa [g₄])
  simp only [W₀, W₁, W₂, W₃, W₄, W₅, finrank_ulift] at this
  apply this <;>
  simpa only [g₀, g₁, g₂, g₃, g₄, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
⊢ g₂ (i₂ x) = i₃ (f₂ x)

Tactic:
simpa using DFunLike.congr_fun hc₂ x

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ Multiplicative.ofAdd (if decide (p x) = true then 1 else 0) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Tactic:
apply_ite (Multiplicative.ofAdd)

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
⊢ (s.lcm f).factorization p = s.sup fun a ↦ (f a).factorization p

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
⊢ n < (f * f').natDegree → (f * f').coeff n ∈ 𝓟

Tactic:
hn

Goal state after:
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
⊢ (f * f').coeff n ∈ 𝓟