harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem span_preimage_le (f : F) (s : Set M₂) :
    span R (f ⁻¹' s) ≤ (span R₂ s).comap f

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F σ₁₂ M M₂
f : F
s : Set M₂
⊢ span R (⇑f ⁻¹' s) ≤ comap f (span R₂ s)

Tactic:
rw [span_le, comap_coe]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F σ₁₂ M M₂
f : F
s : Set M₂
⊢ ⇑f ⁻¹' s ⊆ ⇑f ⁻¹' ↑(span R₂ s)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F σ₁₂ M M₂
f : F
s : Set M₂
⊢ ⇑f ⁻¹' s ⊆ ⇑f ⁻¹' ↑(span R₂ s)

Tactic:
exact preimage_mono subset_span

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem pi_empty (H : ∀ i, Subgroup (f i)) : pi ∅ H = ⊤ :=
  ext fun x => by simp [mem_pi]

Proof state:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
x : (i : η) → f i
⊢ x ∈ pi ∅ H ↔ x ∈ ⊤

Tactic:
simp [mem_pi]

Result:
no goals
-- Mathlib/Topology/Homotopy/Contractible.lean
theorem contractible_iff_id_nullhomotopic (Y : Type*) [TopologicalSpace Y] :
    ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic

Proof state:
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : ContractibleSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic

Tactic:
apply id_nullhomotopic

Result:
no goals

Proof state:
case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic → ContractibleSpace Y

Tactic:
rintro ⟨p, h⟩

Result:
case mpr.intro
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ContractibleSpace Y

Proof state:
case mpr.intro.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ((const Y ()).comp (const Unit p)).Homotopic (ContinuousMap.id Unit)

Tactic:
convert Homotopic.refl (ContinuousMap.id Unit)

Result:
no goals

Proof state:
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic

Tactic:
constructor

Result:
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → (ContinuousMap.id Y).Nullhomotopic

case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic → ContractibleSpace Y

Proof state:
case mpr.intro
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ContractibleSpace Y

Tactic:
refine
  { hequiv_unit' :=
      ⟨{  toFun := ContinuousMap.const _ ()
          invFun := ContinuousMap.const _ p
          left_inv := ?_
          right_inv := ?_ }⟩ }

Result:
case mpr.intro.refine_1
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ((const Unit p).comp (const Y ())).Homotopic (ContinuousMap.id Y)

case mpr.intro.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ((const Y ()).comp (const Unit p)).Homotopic (ContinuousMap.id Unit)

Proof state:
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → (ContinuousMap.id Y).Nullhomotopic

Tactic:
intro

Result:
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : ContractibleSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic

Proof state:
case mpr.intro.refine_1
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ((const Unit p).comp (const Y ())).Homotopic (ContinuousMap.id Y)

Tactic:
exact h.symm

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
@[simp]
lemma localizationAway_jacobian : (localizationAway S r).jacobian = algebraMap R S r

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (localizationAway S r).jacobian = (algebraMap R S) r

Tactic:
rw [jacobian_eq_jacobiMatrix_det, localizationAway_jacobiMatrix]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap (localizationAway S r).Ring S) (Matrix.diagonal fun x => C r).det = (algebraMap R S) r

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap (localizationAway S r).Ring S) (Matrix.diagonal fun x => C r).det = (algebraMap R S) r

Tactic:
simp [show Fintype.card (localizationAway r (S := S)).rels = 1 from rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_lt {x y : BitVec n} : ¬ x < y ↔ y ≤ x

Proof state:
n : Nat
x y : BitVec n
⊢ ¬x < y ↔ y ≤ x

Tactic:
simp [le_def, lt_def]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_smul_sphere (c : G) (x : X) (r : ℝ) :
    (c • ·) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Proof state:
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x => c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_sphere]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppScalarRight_symm_apply_single (i : ι) (m : M) :
    (finsuppScalarRight R M ι).symm (Finsupp.single i m) =
      m ⊗ₜ[R] (Finsupp.single i 1)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
m : M
⊢ (finsuppScalarRight R M ι).symm (Finsupp.single i m) = m ⊗ₜ[R] Finsupp.single i 1

Tactic:
simp [finsuppScalarRight, finsuppRight_symm_apply_single]

Result:
no goals
-- Mathlib/Order/Bounds/OrderIso.lean
theorem isLUB_preimage {s : Set β} {x : α} : IsLUB (f ⁻¹' s) x ↔ IsLUB s (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB (⇑f ⁻¹' s) x ↔ IsLUB s (f x)

Tactic:
rw [← f.symm_symm, ← image_eq_preimage, isLUB_image]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem le_caratheodory [MeasurableSpace X] [BorelSpace X] (hm : IsMetric μ) :
    ‹MeasurableSpace X› ≤ μ.caratheodory

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
μ : OuterMeasure X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
hm : μ.IsMetric
⊢ inst✝¹ ≤ μ.caratheodory

Tactic:
rw [BorelSpace.measurable_eq (α := X)]

Result:
X : Type u_2
inst✝² : EMetricSpace X
μ : OuterMeasure X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
μ : OuterMeasure X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory

Tactic:
exact hm.borel_le_caratheodory

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem map_iInf {ι : Sort*} [Nonempty ι]
    [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F)
    (hf : Function.Injective f) (S : ι → NonUnitalStarSubalgebra R A) :
    ((⨅ i, S i).map f : NonUnitalStarSubalgebra R B) = ⨅ i, (S i).map f

Proof state:
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : NonUnitalSemiring A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module R A
inst✝¹² : NonUnitalSemiring B
inst✝¹¹ : StarRing B
inst✝¹⁰ : Module R B
inst✝⁹ : FunLike F A B
inst✝⁸ : NonUnitalAlgHomClass F R A B
inst✝⁷ : StarHomClass F A B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
ι : Sort u_1
inst✝³ : Nonempty ι
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalStarSubalgebra R A
⊢ map f (⨅ i, S i) = ⨅ i, map f (S i)

Tactic:
apply SetLike.coe_injective

Result:
case a
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : NonUnitalSemiring A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module R A
inst✝¹² : NonUnitalSemiring B
inst✝¹¹ : StarRing B
inst✝¹⁰ : Module R B
inst✝⁹ : FunLike F A B
inst✝⁸ : NonUnitalAlgHomClass F R A B
inst✝⁷ : StarHomClass F A B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
ι : Sort u_1
inst✝³ : Nonempty ι
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalStarSubalgebra R A
⊢ ↑(map f (⨅ i, S i)) = ↑(⨅ i, map f (S i))

Proof state:
case a
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : NonUnitalSemiring A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module R A
inst✝¹² : NonUnitalSemiring B
inst✝¹¹ : StarRing B
inst✝¹⁰ : Module R B
inst✝⁹ : FunLike F A B
inst✝⁸ : NonUnitalAlgHomClass F R A B
inst✝⁷ : StarHomClass F A B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
ι : Sort u_1
inst✝³ : Nonempty ι
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalStarSubalgebra R A
⊢ ↑(map f (⨅ i, S i)) = ↑(⨅ i, map f (S i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ S)

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma one_le_krullDim_iff : 1 ≤ krullDim α ↔ ∃ x y : α, x < y

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ 1 ≤ krullDim α ↔ ∃ x y, x < y

Tactic:
rw [← krullDim_pos_iff, ← Nat.cast_zero, ← WithBot.add_one_le_iff, Nat.cast_zero, zero_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem prod_bot : (prod ⊥ ⊥ : Submodule R (M × M')) = ⊥

Proof state:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_9
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
⊢ ⊥.prod ⊥ = ⊥

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_9
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x : M
y : M'
⊢ (x, y) ∈ ⊥.prod ⊥ ↔ (x, y) ∈ ⊥

Proof state:
case h.mk
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_9
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x : M
y : M'
⊢ (x, y) ∈ ⊥.prod ⊥ ↔ (x, y) ∈ ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Construction.lean
@[reassoc (attr := simp)]
lemma ρFunctorObj_π : ρFunctorObj f πX ≫ πFunctorObj f πX = π'FunctorObj f πX

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
⊢ ρFunctorObj f πX ≫ πFunctorObj f πX = π'FunctorObj f πX

Tactic:
simp [πFunctorObj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eq_getValueCast? [BEq α] [LawfulBEq α] {β : Type v} {l : List ((_ : α) × β)}
    {a : α} : getValue? a l = getValueCast? a l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type v
l : List ((_ : α) × β)
a : α
⊢ getValue? a l = getValueCast? a l

Tactic:
induction l using assoc_induction <;> simp_all [getValueCast?_cons, getValue?_cons]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Coherence.lean
theorem preinclusion_map₂ {a b : B} (f g : Discrete (Path.{v + 1} a b)) (η : f ⟶ g) :
    (preinclusion B).map₂ η = eqToHom (congr_arg _ (Discrete.ext (Discrete.eq_of_hom η)))

Proof state:
case up.up
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ (preinclusion B).map₂ { down := { down := down✝ } } = eqToHom ⋯

Tactic:
cases Discrete.ext (by assumption)

Result:
case up.up.refl
B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
down✝ : f.as = f.as
⊢ (preinclusion B).map₂ { down := { down := down✝ } } = eqToHom ⋯

Proof state:
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
η : f ⟶ g
⊢ (preinclusion B).map₂ η = eqToHom ⋯

Tactic:
rcases η with ⟨⟨⟩⟩

Result:
case up.up
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ (preinclusion B).map₂ { down := { down := down✝ } } = eqToHom ⋯

Proof state:
case up.up.refl
B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
down✝ : f.as = f.as
⊢ (preinclusion B).map₂ { down := { down := down✝ } } = eqToHom ⋯

Tactic:
convert (inclusionPath a b).map_id _

Result:
no goals

Proof state:
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ Discrete.as ?m.4824 = Discrete.as ?m.4825

Tactic:
assumption

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
theorem isUnit_ι_of_isUnit {m : M} (h : IsUnit (Q m)) : IsUnit (ι Q m)

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit (Q m)
val✝ : Invertible (Q m)
this : Invertible ((ι Q) m) := invertibleιOfInvertible Q m
⊢ IsUnit ((ι Q) m)

Tactic:
exact isUnit_of_invertible (ι Q m)

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit (Q m)
val✝ : Invertible (Q m)
⊢ IsUnit ((ι Q) m)

Tactic:
letI := invertibleιOfInvertible Q m

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit (Q m)
val✝ : Invertible (Q m)
this : Invertible ((ι Q) m) := invertibleιOfInvertible Q m
⊢ IsUnit ((ι Q) m)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit (Q m)
⊢ IsUnit ((ι Q) m)

Tactic:
cases h.nonempty_invertible

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit (Q m)
val✝ : Invertible (Q m)
⊢ IsUnit ((ι Q) m)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le.intro_sub {a b : Int} (n : Nat) (h : b - a = n) : a ≤ b

Proof state:
a b : Int
n : Nat
h : b - a = ↑n
⊢ (↑n).NonNeg

Tactic:
constructor

Result:
no goals

Proof state:
a b : Int
n : Nat
h : b - a = ↑n
⊢ a ≤ b

Tactic:
simp [le_def, h]

Result:
a b : Int
n : Nat
h : b - a = ↑n
⊢ (↑n).NonNeg
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_apply (w : InfinitePlace K) (x : K) :
    normAtPlace w (mixedEmbedding K x) = w x

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ (normAtPlace w) ((mixedEmbedding K) x) = w x

Tactic:
simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, mixedEmbedding,
  RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite,
  ite_id]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem map_mul : (p * q).map f = p.map f * q.map f

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ map f (p * q) = map f p * map f q

Tactic:
rw [map, eval₂_mul_noncomm]

Result:
case hf
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ ∀ (k : ℕ), Commute ((C.comp f) (q.coeff k)) X

Proof state:
case hf
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ ∀ (k : ℕ), Commute ((C.comp f) (q.coeff k)) X

Tactic:
exact fun k => (commute_X _).symm

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
lemma rewrites_of_exists_parts (r : ContextFreeRule T N) (p q : List (Symbol T N)) :
    r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Proof state:
case nil
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
⊢ r.Rewrites ([] ++ [Symbol.nonterminal r.input] ++ q) ([] ++ r.output ++ q)

Tactic:
exact Rewrites.head q

Result:
no goals

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Tactic:
induction p with
| nil         => exact Rewrites.head q
| cons d l ih => exact Rewrites.cons d ih

Result:
no goals

Proof state:
case cons
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
d : Symbol T N
l : List (Symbol T N)
ih : r.Rewrites (l ++ [Symbol.nonterminal r.input] ++ q) (l ++ r.output ++ q)
⊢ r.Rewrites (d :: l ++ [Symbol.nonterminal r.input] ++ q) (d :: l ++ r.output ++ q)

Tactic:
exact Rewrites.cons d ih

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_preΨ_le (n : ℤ) : (W.preΨ n).natDegree ≤
    (n.natAbs ^ 2 - if Even n then 4 else 1) / 2

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.preΨ n).natDegree ≤ (n.natAbs ^ 2 - if Even n then 4 else 1) / 2

Tactic:
induction n using Int.negInduction with
| nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n
| neg ih => simp only [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_neg, ih]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).natDegree ≤ ((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2
n✝ : ℕ
⊢ (W.preΨ (-↑n✝)).natDegree ≤ ((-↑n✝).natAbs ^ 2 - if Even (-↑n✝) then 4 else 1) / 2

Tactic:
simp only [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_neg, ih]

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.preΨ ↑n).natDegree ≤ ((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2

Tactic:
exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_attachWith (l : Vector α n) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
    pmap f (l.attachWith q H₁) H₂ =
      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩)

Proof state:
α : Type u_1
n : Nat
q : α → Prop
β : Type u_2
l : Vector α n
p : { x // q x } → Prop
f : (a : { x // q x }) → p a → β
H₁ : ∀ (x : α), x ∈ l → q x
H₂ : ∀ (a : { x // q x }), a ∈ l.attachWith q H₁ → p a
⊢ pmap f (l.attachWith q H₁) H₂ = pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type ?u.33121
n : Nat
q : α → Prop
β : Type ?u.33151
l : Vector α n
p : { x // q x } → Prop
f : (a : { x // q x }) → p a → β
H₁ : ∀ (x : α), x ∈ l → q x
H₂ : ∀ (a : { x // q x }), a ∈ l.attachWith q H₁ → p a
a : α
h : a ∈ l
⊢ ⟨a, ⋯⟩ ∈ l.attachWith q H₁

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma generatingMonomorphisms_le_monomorphisms (G : C) :
    generatingMonomorphisms G ≤ MorphismProperty.monomorphisms C

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : C
⊢ generatingMonomorphisms G ≤ MorphismProperty.monomorphisms C

Tactic:
rintro _ _ _ ⟨X⟩

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
G X✝ Y : C
X : Subobject G
⊢ MorphismProperty.monomorphisms C X.arrow

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
G X✝ Y : C
X : Subobject G
⊢ MorphismProperty.monomorphisms C X.arrow

Tactic:
exact inferInstanceAs (Mono _)

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
lemma ChartedSpace.sum_chartAt_inr (x' : M') :
    haveI : Nonempty H := nonempty_of_chartedSpace x'
    chartAt H (Sum.inr x')
      = (chartAt H x').lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inr

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x' : M'
⊢ chartAt H (Sum.inr x') = (chartAt H x').lift_openEmbedding ⋯

Tactic:
simp only [chartAt, sum, nonempty_of_chartedSpace x', ↓reduceDIte]

Result:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x' : M'
⊢ ChartedSpace.chartAt (Sum.inr x') = (ChartedSpace.chartAt x').lift_openEmbedding ⋯

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x' : M'
⊢ ChartedSpace.chartAt (Sum.inr x') = (ChartedSpace.chartAt x').lift_openEmbedding ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_sub (x y : M) : Q (x - y) = Q (y - x)

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ Q (x - y) = Q (y - x)

Tactic:
rw [← neg_sub, map_neg]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_self {n} {i : Fin (n + 1)} : X.σ i ≫ X.δ (Fin.castSucc i) = 𝟙 _

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

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _⦋n⦌)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _⦋n⦌)

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_self, op_id, X.map_id]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem coeff_truncFun' (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) :
    (truncFun' n φ).coeff m = if m ≤ n then coeff R m φ else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun' n φ) = if m ≤ n then (coeff R m) φ else 0

Tactic:
simp [truncFun', MvPolynomial.coeff_sum]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun' n φ) = if m ≤ n then (coeff R m) φ else 0

Tactic:
classical
simp [truncFun', MvPolynomial.coeff_sum]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_unop [T2Space 𝔸] (x : 𝔸ᵐᵒᵖ) :
    exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (exp 𝕂 x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸ᵐᵒᵖ
⊢ exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (exp 𝕂 x)

Tactic:
simp_rw [exp, expSeries_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]

Result:
no goals