harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Flat/Basic.lean
theorem includeRight_injective [Module.Flat R B] (ha : Function.Injective (algebraMap R A)) :
    Function.Injective (includeRight : B →ₐ[R] A ⊗[R] B)

Proof state:
R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
⊢ Function.Injective ⇑includeRight

Tactic:
convert Module.Flat.rTensor_preserves_injective_linearMap (M := B) (Algebra.linearMap R A) ha
  |>.comp (_root_.TensorProduct.lid R B).symm.injective

Result:
case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
⊢ ⇑includeRight = ⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm

Proof state:
case h.e'_3.h
R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
x✝ : B
⊢ includeRight x✝ = (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm) x✝

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
⊢ ⇑includeRight = ⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm

Tactic:
ext

Result:
case h.e'_3.h
R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
x✝ : B
⊢ includeRight x✝ = (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm) x✝
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_monomial_le {d : σ →₀ ℕ} (c : R) :
    m.degree (monomial d c) ≼[m] d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ {d}.sup ⇑m.toSyn ≤ m.toSyn d

Tactic:
simp only [Finset.sup_singleton, le_refl]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ ((monomial d) c).support.sup ⇑m.toSyn ≤ m.toSyn d

Tactic:
apply le_trans (Finset.sup_mono support_monomial_subset)

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ {d}.sup ⇑m.toSyn ≤ m.toSyn d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.toSyn (m.degree ((monomial d) c)) ≤ m.toSyn d

Tactic:
simp only [degree, AddEquiv.apply_symm_apply]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ ((monomial d) c).support.sup ⇑m.toSyn ≤ m.toSyn d
-- Mathlib/NumberTheory/AbelSummation.lean
theorem _root_.sum_mul_eq_sub_sub_integral_mul' {n m : ℕ} (h : n ≤ m)
    (hf_diff : ∀ t ∈ Set.Icc (n : ℝ) m, DifferentiableAt ℝ f t)
    (hf_int : IntegrableOn (deriv f) (Set.Icc (n : ℝ) m)) :
    ∑ k ∈ Ioc n m, f k * c k =
      f m * (∑ k ∈ Icc 0 m, c k) - f n * (∑ k ∈ Icc 0 n, c k) -
        ∫ t in Set.Ioc (n : ℝ) m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Proof state:
case h.e'_2.h.h.e'_4
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ n = ⌊↑n⌋₊

case h.e'_2.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_6.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ n = ⌊↑n⌋₊

Tactic:
all_goals rw [Nat.floor_natCast]

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_6.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ n = ⌊↑n⌋₊

Tactic:
rw [Nat.floor_natCast]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ ∑ k ∈ Ioc n m, f ↑k * c k =
    f ↑m * ∑ k ∈ Icc 0 m, c k - f ↑n * ∑ k ∈ Icc 0 n, c k -
      ∫ (t : ℝ) in Set.Ioc ↑n ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
convert sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int

Result:
case h.e'_2.h.h.e'_4
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ n = ⌊↑n⌋₊

case h.e'_2.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_6.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ n = ⌊↑n⌋₊
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem Disjoint.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p)
    {σ τ : Perm α} (h : Disjoint σ τ) : Disjoint (σ.extendDomain f) (τ.extendDomain f)

Proof state:
case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : σ.Disjoint τ
b : β
pb : p b
h : τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩
⊢ (τ.extendDomain f) b = b

Tactic:
rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]

Result:
no goals

Proof state:
case neg.h
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b

Tactic:
rw [extendDomain_apply_not_subtype _ _ pb]

Result:
no goals

Proof state:
case neg
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b

Tactic:
left

Result:
case neg.h
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b

Proof state:
case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (τ.extendDomain f) b = b

Tactic:
intro h

Result:
case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : σ.Disjoint τ
b : β
pb : p b
h : τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩
⊢ (τ.extendDomain f) b = b

Proof state:
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
⊢ (σ.extendDomain f).Disjoint (τ.extendDomain f)

Tactic:
intro b

Result:
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b

Proof state:
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b

Tactic:
by_cases pb : p b

Result:
case pos
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b

case neg
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S : Solution`, we have that
`S.Y ^ 3 + (S.u₄ * S.Z) ^ 3 = S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3`. -/
private lemma formula3 :
    S.Y ^ 3 + (S.u₄ * S.Z) ^ 3 = S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 :=
  calc S.Y^3+(S.u₄*S.Z)^3=S.Y^3+S.u₄^2*S.u₄*S.Z^3

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
      ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) ^ 2 * ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) *
        FermatLastTheoremForThreeGen.Solution.Z S ^ 3 =
    FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
      ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3

Tactic:
simp [← Units.val_pow_eq_pow_val, S.u₄_sq]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
      (↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S) ^ 3 =
    FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
      ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) ^ 2 * ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) *
        FermatLastTheoremForThreeGen.Solution.Z S ^ 3

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_finset_sup_eq_iInter (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ}
    (hr : 0 < r) : ball (s.sup p) x r = ⋂ i ∈ s, ball (p i) x r

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = ⋂ i ∈ s, (p i).ball x r

Tactic:
lift r to NNReal using hr.le

Result:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < ↑r
⊢ (s.sup p).ball x ↑r = ⋂ i ∈ s, (p i).ball x ↑r

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < ↑r
⊢ (s.sup p).ball x ↑r = ⋂ i ∈ s, (p i).ball x ↑r

Tactic:
simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
  Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_le_max_of_aleph0_le_right {a b : Cardinal} (h : ℵ₀ ≤ b) : a * b ≤ max a b

Proof state:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ b
⊢ a * b ≤ a ⊔ b

Tactic:
simpa only [mul_comm b, max_comm b] using mul_le_max_of_aleph0_le_left h

Result:
no goals
-- Mathlib/Order/LatticeIntervals.lean
protected lemma codisjoint_iff [SemilatticeSup α] {x y : Iic a} :
    Codisjoint x y ↔ (x : α) ⊔ (y : α) = a

Proof state:
α : Type u_1
a : α
inst✝ : SemilatticeSup α
x y : ↑(Iic a)
⊢ Codisjoint x y ↔ ↑x ⊔ ↑y = a

Tactic:
simpa only [_root_.codisjoint_iff] using Iic.eq_top_iff

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_dirac' [MeasurableSpace α] (f : α → E) (a : α) (hfm : StronglyMeasurable f) :
    ∫ x, f x ∂Measure.dirac a = f a

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
borelize E

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ ∫ (x : α), f a ∂Measure.dirac a = f a

Tactic:
simp [Measure.dirac_apply_of_mem]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
calc
  ∫ x, f x ∂Measure.dirac a = ∫ _, f a ∂Measure.dirac a :=
    integral_congr_ae <| ae_eq_dirac' hfm.measurable
  _ = f a := by simp [Measure.dirac_apply_of_mem]

Result:
no goals
-- Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean
/-- For a global integral curve `γ`, if it crosses itself at `a b : ℝ`, then it is periodic with
period `a - b`. -/
lemma IsIntegralCurve.periodic_of_eq [BoundarylessManifold I M]
    (hγ : IsIntegralCurve γ v)
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))
    (heq : γ a = γ b) : Periodic γ (a - b)

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
a b : ℝ
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
heq : γ a = γ b
t : ℝ
⊢ (γ ∘ fun x => x + (a - b)) b = γ b

Tactic:
rw [comp_apply, add_sub_cancel, heq]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
a b : ℝ
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
heq : γ a = γ b
t : ℝ
⊢ γ (t + (a - b)) = γ t

Tactic:
apply congrFun <|
  isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (t₀ := b) hv (hγ.comp_add _) hγ _

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
a b : ℝ
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
heq : γ a = γ b
t : ℝ
⊢ (γ ∘ fun x => x + (a - b)) b = γ b

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
a b : ℝ
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
heq : γ a = γ b
⊢ Periodic γ (a - b)

Tactic:
intro t

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
a b : ℝ
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
heq : γ a = γ b
t : ℝ
⊢ γ (t + (a - b)) = γ t
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem map_modByMonicHom (h : IsAdjoinRootMonic S f) (x : S) : h.map (h.modByMonicHom x) = x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
⊢ h.map (h.repr x %ₘ f) = x

Tactic:
rw [map_modByMonic, map_repr]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
⊢ h.map (h.modByMonicHom x) = x

Tactic:
rw [modByMonicHom, LinearMap.coe_mk]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
⊢ h.map ({ toFun := fun x => h.repr x %ₘ f, map_add' := ⋯ } x) = x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
⊢ h.map ({ toFun := fun x => h.repr x %ₘ f, map_add' := ⋯ } x) = x

Tactic:
dsimp

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
⊢ h.map (h.repr x %ₘ f) = x
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma ΨSq_neg (n : ℤ) : W.ΨSq (-n) = W.ΨSq n

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ W.ΨSq (-n) = W.ΨSq n

Tactic:
simp only [ΨSq, preΨ_neg, neg_sq, even_neg]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
lemma evaluation_ne_zero_iff_mem_basicOpen (x : U) (f : X.presheaf.obj (op U)) :
    X.evaluation x f ≠ 0 ↔ x.val ∈ X.toRingedSpace.basicOpen f

Proof state:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f ≠ 0 ↔ ↑x ∈ X.toRingedSpace.basicOpen f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem lowerCentralSeries_map_eq_lcs : (lowerCentralSeries R L N k).map N.incl = N.lcs k

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ lcs k N ≤ N

Tactic:
apply lcs_le_self

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ map N.incl (lowerCentralSeries R L (↥N) k) = lcs k N

Tactic:
rw [lowerCentralSeries_eq_lcs_comap, LieSubmodule.map_comap_incl, inf_eq_right]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ lcs k N ≤ N
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubring R} {x : R} :
    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
S : ι → NonUnitalSubring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem coe_sigma (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
    (@Multiset.sigma α σ l₁ fun a => l₂ a) = l₁.sigma l₂

Proof state:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).sigma fun a => ↑(l₂ a)) = ↑(l₁.sigma l₂)

Tactic:
rw [Multiset.sigma, List.sigma, ← coe_bind]

Result:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a => map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a => ↑(List.map (Sigma.mk a) (l₂ a))

Proof state:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a => map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a => ↑(List.map (Sigma.mk a) (l₂ a))

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_sUnion_of_directed {s : Set (Set A)} (hsn : s.Nonempty)
    (hs : DirectedOn (· ⊆ ·) s) (h : ∀ a ∈ s, AlgebraicIndependent R ((↑) : a → A)) :
    AlgebraicIndependent R ((↑) : ⋃₀ s → A)

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val

Tactic:
letI : Nonempty s := Nonempty.to_subtype hsn

Result:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val

Tactic:
exact algebraicIndependent_iUnion_of_directed hs.directed_val (by simpa using h)

Result:
no goals

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ ∀ (i : ↑s), AlgebraicIndependent R Subtype.val

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem nsmul_modEq_nsmul [NoZeroSMulDivisors ℕ α] (hn : n ≠ 0) :
    n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p] :=
  exists_congr fun m => by rw [← smul_sub, smul_comm, smul_right_inj hn]

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
p a b : α
n : ℕ
inst✝ : NoZeroSMulDivisors ℕ α
hn : n ≠ 0
m : ℤ
⊢ n • b - n • a = m • n • p ↔ b - a = m • p

Tactic:
rw [← smul_sub, smul_comm, smul_right_inj hn]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.le_right_of_left_le (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment 𝕜 x y) (hxz : f x ≤ f z) : f z ≤ f y

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y

Tactic:
exact hf.le_right_of_left_le' hx hy ha.le hb hab hxz

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x ≤ f z
⊢ f z ≤ f y

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem sum_mul {S : Type*} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoidAlgebra k G)
    {f : G → k → S} : s.sum f * b = s.sum fun a c ↦ f a c * b

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : SkewMonoidAlgebra k G
f : G → k → S
⊢ s.sum f * b = s.sum fun a c => f a c * b

Tactic:
simp only [sum, Finsupp.sum, Finset.sum_mul]

Result:
no goals