harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ → EReal) :=
  coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe_eq_Ioo]; exact ordConnected_Ioo

Proof state:
⊢ (Ioo ⊥ ⊤).OrdConnected

Tactic:
exact ordConnected_Ioo

Result:
no goals

Proof state:
⊢ (range Real.toEReal).OrdConnected

Tactic:
rw [range_coe_eq_Ioo]

Result:
⊢ (Ioo ⊥ ⊤).OrdConnected
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem Basis.opNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ}
    (hM : 0 ≤ M) (hu : ∀ i, ‖u (v i)‖ ≤ M) :
    ‖u‖ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖ * M

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
hu : ∀ (i : ι), ‖u (v i)‖ ≤ M
⊢ ‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M

Tactic:
simpa using NNReal.coe_le_coe.mpr (v.opNNNorm_le ⟨M, hM⟩ hu)

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_bot_of_isLocalized₀_span {N : Submodule R M}
    (h : ∀ r : s, N.localized₀ (.powers r.1) (f r) = ⊥) : N = ⊥ :=
  eq_of_isLocalized₀_span s span_eq Mₚ f fun _ ↦ by simp only [h, Submodule.localized₀_bot]

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
N : Submodule R M
h : ∀ (r : ↑s), localized₀ (Submonoid.powers ↑r) (f r) N = ⊥
x✝ : ↑s
⊢ localized₀ (Submonoid.powers ↑x✝) (f x✝) N = localized₀ (Submonoid.powers ↑x✝) (f x✝) ⊥

Tactic:
simp only [h, Submodule.localized₀_bot]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_finTwoArrow {α : Type u} {m : MeasurableSpace α} (μ : Measure α)
    [SigmaFinite μ] :
    MeasurePreserving MeasurableEquiv.finTwoArrow (Measure.pi fun _ => μ) (μ.prod μ)

Proof state:
α : Type u
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi fun x => μ) (μ.prod μ)

Tactic:
simpa only [Matrix.vec_single_eq_const, Matrix.vecCons_const] using
  measurePreserving_finTwoArrow_vec μ μ

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem LieAlgebra.nilpotent_of_nilpotent_quotient {I : LieIdeal R L} (h₁ : I ≤ center R L)
    (h₂ : IsNilpotent (L ⧸ I)) : IsNilpotent L

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ k, lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
k : ℕ
hk : lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ lowerCentralSeries R L (L ⧸ I) k = ⊥

Tactic:
simp [← LieSubmodule.toSubmodule_inj, coe_lowerCentralSeries_ideal_quot_eq, hk]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ k, lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ ∃ k, lowerCentralSeries R L (L ⧸ I) k = ⊥

Tactic:
peel h₂ with k hk

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ k, lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
k : ℕ
hk : lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ lowerCentralSeries R L (L ⧸ I) k = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent (L ⧸ I)
⊢ LieModule.IsNilpotent L (L ⧸ I)

Tactic:
simp only [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₂ ⊢

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ k, lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ ∃ k, lowerCentralSeries R L (L ⧸ I) k = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent (L ⧸ I)
this : LieModule.IsNilpotent L (L ⧸ I)
⊢ LieRing.IsNilpotent L

Tactic:
exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent (L ⧸ I)
⊢ LieRing.IsNilpotent L

Tactic:
suffices LieModule.IsNilpotent L (L ⧸ I) by
  exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent (L ⧸ I)
⊢ LieModule.IsNilpotent L (L ⧸ I)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_coe_pi : tan (π : Angle) = 0

Proof state:
⊢ (↑π).tan = 0

Tactic:
rw [tan_coe, Real.tan_pi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
    get! m a = (get? m a).get!

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ get! m a = (get? m a).get!

Tactic:
simp_to_model using List.getValue!_eq_getValue?

Result:
no goals
-- Mathlib/RingTheory/KrullDimension/Basic.lean
lemma Ring.krullDimLE_zero_iff : Ring.KrullDimLE 0 R ↔ ∀ I : Ideal R, I.IsPrime → I.IsMaximal

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime), ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_zero,
  Order.krullDim_nonpos_iff_forall_isMax,
  (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall, PrimeSpectrum.isMax_iff]

Result:
R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime), ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem xa_sq (i : ZMod (2 * n)) : xa i ^ 2 = a n

Proof state:
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 2 = a ↑n

Tactic:
simp [sq]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem _root_.Batteries.RBNode.zoom_toList {t : RBNode α} (eq : t.zoom cut = (t', p')) :
    p'.withList t'.toList = t.toList

Proof state:
α : Type u_1
cut : α → Ordering
t' : RBNode α
p' : Path α
t : RBNode α
eq : zoom cut t = (t', p')
⊢ (root.fill t).toList = t.toList

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
t' : RBNode α
p' : Path α
t : RBNode α
eq : zoom cut t = (t', p')
⊢ p'.withList t'.toList = t.toList

Tactic:
rw [← fill_toList, ← zoom_fill eq]

Result:
α : Type u_1
cut : α → Ordering
t' : RBNode α
p' : Path α
t : RBNode α
eq : zoom cut t = (t', p')
⊢ (root.fill t).toList = t.toList
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
    DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter ht]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem eq_iSup_inf_genEigenspace [FiniteDimensional K V] (k : ℕ∞)
    (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, f.genEigenspace μ k = ⊤) :
    p = ⨆ μ, p ⊓ f.genEigenspace μ k

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ p = ⨆ μ, p ⊓ (f.genEigenspace μ) k

Tactic:
rw [← inf_iSup_genEigenspace h, h', inf_top_eq]

Result:
no goals
-- Mathlib/Data/Analysis/Topology.lean
theorem ofEquiv_val (E : σ ≃ τ) (F : Ctop α σ) (a : τ) : F.ofEquiv E a = F (E.symm a)

Proof state:
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
F : Ctop α σ
a : τ
⊢ (ofEquiv E F).f a = F.f (E.symm a)

Tactic:
cases F

Result:
case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ (ofEquiv E
          { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
            inter_sub := inter_sub✝ }).f
      a =
    { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }.f
      (E.symm a)

Proof state:
case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ (ofEquiv E
          { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
            inter_sub := inter_sub✝ }).f
      a =
    { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }.f
      (E.symm a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_mul_C : (p * C a).eval₂ f g = p.eval₂ f g * f a :=
  (eval₂_mul_monomial _ _).trans <| by simp

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
a : R
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ (eval₂ f g p * f a * Finsupp.prod 0 fun n e => g n ^ e) = eval₂ f g p * f a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_sub_nat (a : α) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌊a - ↑n⌋ = ⌊a⌋ - ↑n

Tactic:
rw [← Int.cast_natCast, floor_sub_int]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem diagramNatTrans_comp {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C) :
    J.diagramNatTrans (η ≫ γ) X = J.diagramNatTrans η X ≫ J.diagramNatTrans γ X

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (η ≫ γ) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i =
    (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i

Tactic:
simp

Result:
no goals

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans (η ≫ γ) X).app x✝ = (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X).app x✝

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (η ≫ γ) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i =
    (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
⊢ J.diagramNatTrans (η ≫ γ) X = J.diagramNatTrans η X ≫ J.diagramNatTrans γ X

Tactic:
ext : 2

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans (η ≫ γ) X).app x✝ = (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X).app x✝
-- Mathlib/AlgebraicGeometry/ResidueField.lean
lemma descResidueField_fromSpecResidueField {K : Type*} [Field K] (X : Scheme) {x}
    (f : X.presheaf.stalk x ⟶ .of K) [IsLocalHom f.hom] :
    Spec.map (X.descResidueField f) ≫
      X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x

Proof state:
K : Type u_1
inst✝¹ : Field K
X : Scheme
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ CommRingCat.of K
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
⊢ Spec.map (descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x

Tactic:
simp [fromSpecResidueField, ← Spec.map_comp_assoc]

Result:
no goals
-- Mathlib/Algebra/Field/Rat.lean
lemma num_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.num = q.den

Proof state:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Tactic:
simpa using q.coprime_num_den.symm

Result:
no goals

Proof state:
q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.num = q.den

Tactic:
rw [inv_def, divNat, num, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq),
  Int.natAbs_ofNat]

Result:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_zpow_exp_pos_mul_atTop (k : ℤ) {b : ℝ} (hb : 0 < b) :
    (fun x : ℝ => x ^ k) =o[atTop] fun x => exp (b * x)

Proof state:
k : ℤ
b : ℝ
hb : 0 < b
⊢ (fun x => x ^ k) =o[atTop] fun x => rexp (b * x)

Tactic:
simpa only [Real.rpow_intCast] using isLittleO_rpow_exp_pos_mul_atTop k hb

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Prime.factorization_self {p : ℕ} (hp : Prime p) : p.factorization p = 1

Proof state:
p : ℕ
hp : Prime p
⊢ p.factorization p = 1

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Refinements.lean
lemma ShortComplex.Exact.exact_up_to_refinements
    (hS : S.Exact) {A : C} (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0) :
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
exact hS x₂ hx₂

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
-- Mathlib/Algebra/Module/Lattice.lean
/-- Any lattice has `R`-rank equal to the `K`-rank of `V`. -/
lemma rank' [IsFractionRing R K] (M : Submodule R V) [IsLattice K M] :
    Module.rank R M = Module.rank K V

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsFractionRing R K
M : Submodule R V
inst✝ : IsLattice K M
⊢ Module.rank R ↥M = Module.rank K V

Tactic:
let b := Module.Free.chooseBasis R M

Result:
R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsFractionRing R K
M : Submodule R V
inst✝ : IsLattice K M
b : Basis (Module.Free.ChooseBasisIndex R ↥M) R ↥M := Module.Free.chooseBasis R ↥M
⊢ Module.rank R ↥M = Module.rank K V

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsFractionRing R K
M : Submodule R V
inst✝ : IsLattice K M
b : Basis (Module.Free.ChooseBasisIndex R ↥M) R ↥M := Module.Free.chooseBasis R ↥M
⊢ Module.rank R ↥M = Module.rank K V

Tactic:
rw [rank_eq_card_basis b, ← rank_eq_card_basis (b.extendOfIsLattice K)]

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) : (map₂ f a b).map g = map₂ f' a (b.map g')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
β' : Type u_6
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ Option.map g (map₂ f a b) = map₂ f' a (Option.map g' b)

Tactic:
cases a <;> cases b <;> simp [h_distrib]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean
theorem equivFun_symm_single [Finite n] (b : Basis n R M) (i : n) :
    b.equivFun.symm (Pi.single i 1) = b i

Proof state:
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite n
b : Basis n R M
i : n
⊢ b.equivFun.symm (Pi.single i 1) = b i

Tactic:
cases nonempty_fintype n

Result:
case intro
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite n
b : Basis n R M
i : n
val✝ : Fintype n
⊢ b.equivFun.symm (Pi.single i 1) = b i

Proof state:
case intro
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite n
b : Basis n R M
i : n
val✝ : Fintype n
⊢ b.equivFun.symm (Pi.single i 1) = b i

Tactic:
simp [Pi.single_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma comp_homologyMap_comp [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂)
    (h₁ : S₁.LeftHomologyData) (h₂ : S₂.RightHomologyData) :
    h₁.π ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom ≫ h₂.ι =
      h₁.i ≫ φ.τ₂ ≫ h₂.p

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.π ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom ≫ h₂.ι = h₁.i ≫ φ.τ₂ ≫ h₂.p

Tactic:
dsimp only [LeftHomologyData.homologyIso, RightHomologyData.homologyIso,
  Iso.symm, Iso.trans, Iso.refl, leftHomologyIso, rightHomologyIso,
  leftHomologyMapIso', rightHomologyMapIso',
  LeftHomologyData.cyclesIso, RightHomologyData.opcyclesIso,
  LeftHomologyData.leftHomologyIso, RightHomologyData.rightHomologyIso,
  homologyMap, homologyMap']

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.π ≫
      (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData ≫
          leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left) ≫
        leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫
          ((S₂.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₂) S₂.homologyData.right S₂.rightHomologyData) ≫
              rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData h₂) ≫
            h₂.ι =
    h₁.i ≫ φ.τ₂ ≫ h₂.p

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.π ≫
      (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData ≫
          leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left) ≫
        leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫
          ((S₂.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₂) S₂.homologyData.right S₂.rightHomologyData) ≫
              rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData h₂) ≫
            h₂.ι =
    h₁.i ≫ φ.τ₂ ≫ h₂.p

Tactic:
simp only [assoc, rightHomologyι_naturality', rightHomologyι_naturality'_assoc,
  leftHomologyπ_naturality'_assoc, HomologyData.comm_assoc, p_opcyclesMap'_assoc,
  id_τ₂, p_opcyclesMap', id_comp, cyclesMap'_i_assoc]

Result:
no goals
-- Mathlib/Data/NNRat/Lemmas.lean
lemma toNNRat_inv (q : ℚ) : toNNRat q⁻¹ = (toNNRat q)⁻¹

Proof state:
case inr
q : ℚ
hq : 0 ≤ q
⊢ (↑q.toNNRat)⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
rw [← coe_inv, toNNRat_coe]

Result:
no goals

Proof state:
case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
nth_rw 1 [← Rat.coe_toNNRat q hq]

Result:
case inr
q : ℚ
hq : 0 ≤ q
⊢ (↑q.toNNRat)⁻¹.toNNRat = q.toNNRat⁻¹

Proof state:
case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]

Result:
no goals

Proof state:
q : ℚ
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
obtain hq | hq := le_total q 0

Result:
case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
-- Mathlib/Data/Seq/Seq.lean
theorem head_eq_destruct (s : Seq α) : head.{u} s = Prod.fst.{u} <$> destruct.{u} s

Proof state:
α : Type u
s : Seq α
⊢ s.head = Prod.fst <$> s.destruct

Tactic:
unfold destruct head

Result:
α : Type u
s : Seq α
⊢ s.get? 0 = Prod.fst <$> (fun a' => (a', s.tail)) <$> s.get? 0

Proof state:
α : Type u
s : Seq α
⊢ s.get? 0 = Prod.fst <$> (fun a' => (a', s.tail)) <$> s.get? 0

Tactic:
cases get? s 0 <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_three_eq_top : cycleGraph 3 = ⊤

Proof state:
⊢ ∀ (x x_1 : Fin 3), (cycleGraph 3).Adj x x_1 = ⊤.Adj x x_1

Tactic:
decide

Result:
no goals

Proof state:
⊢ cycleGraph 3 = ⊤

Tactic:
simp only [SimpleGraph.ext_iff, funext_iff]

Result:
⊢ ∀ (x x_1 : Fin 3), (cycleGraph 3).Adj x x_1 = ⊤.Adj x x_1
-- Mathlib/Data/Int/Log.lean
theorem clog_zpow {b : ℕ} (hb : 1 < b) (z : ℤ) : clog b ((b : R) ^ z : R) = z

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ clog b (↑b ^ z) = z

Tactic:
rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem norm_exp (q : ℍ[ℝ]) : ‖exp ℝ q‖ = ‖exp ℝ q.re‖

Proof state:
q : ℍ
⊢ ‖exp ℝ q‖ = ‖exp ℝ q.re‖

Tactic:
rw [norm_eq_sqrt_real_inner (exp ℝ q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs,
  Real.norm_eq_abs]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_lsub_le {ι} (f : ι → Ordinal) : cof (lsub.{u, u} f) ≤ #ι

Proof state:
ι : Type u
f : ι → Ordinal.{u}
⊢ (lsub f).cof ≤ #ι

Tactic:
rw [cof_eq_sInf_lsub]

Result:
ι : Type u
f : ι → Ordinal.{u}
⊢ sInf {a | ∃ ι_1 f_1, lsub f_1 = lsub f ∧ #ι_1 = a} ≤ #ι

Proof state:
ι : Type u
f : ι → Ordinal.{u}
⊢ sInf {a | ∃ ι_1 f_1, lsub f_1 = lsub f ∧ #ι_1 = a} ≤ #ι

Tactic:
exact csInf_le' ⟨ι, f, rfl, rfl⟩

Result:
no goals