harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
lemma pushouts_le_llp_rlp : T.pushouts ≤ T.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : T.pushouts i
⊢ T.rlp.llp i

Tactic:
exact (T.rlp.llp.isStableUnderCobaseChange_iff_pushouts_le).1 inferInstance i
  (pushouts_monotone T.le_llp_rlp _ hi)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts ≤ T.rlp.llp

Tactic:
intro A B i hi

Result:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : T.pushouts i
⊢ T.rlp.llp i
-- Mathlib/Order/Filter/Pi.lean
theorem map_pi_map_coprodᵢ_le :
    map (fun k : ∀ i, α i => fun i => m i (k i)) (Filter.coprodᵢ f) ≤
      Filter.coprodᵢ fun i => map (m i) (f i)

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => map (m i) (f i)

Tactic:
simp only [le_def, mem_map, mem_coprodᵢ_iff]

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' x

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' x

Tactic:
intro s h i

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s

Proof state:
case intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s

Tactic:
exact ⟨{ x : α i | m i x ∈ t }, H, fun x hx => hH hx⟩

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s

Tactic:
obtain ⟨t, H, hH⟩ := h i

Result:
case intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem ker_le_range_iff {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
    ker g ≤ range f ↔ f.range.mkQ.comp g.ker.subtype = 0

Proof state:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ ker g ≤ range f ↔ (range f).mkQ ∘ₗ (ker g).subtype = 0

Tactic:
rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem coplanar_iff_finrank_le_two {s : Set P} [FiniteDimensional k (vectorSpan k s)] :
    Coplanar k s ↔ finrank k (vectorSpan k s) ≤ 2

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2

Tactic:
exact mod_cast h

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2

Tactic:
have h : Coplanar k s ↔ Module.rank k (vectorSpan k s) ≤ 2 := Iff.rfl

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2

Tactic:
rw [← finrank_eq_rank] at h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2
-- Mathlib/Analysis/Convex/Function.lean
theorem OrderIso.strictConvexOn_symm (f : α ≃o β) (hf : StrictConcaveOn 𝕜 univ f) :
    StrictConvexOn 𝕜 univ f.symm

Proof state:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ a • f x' + b • f y' < f (a • x' + b • y')

Tactic:
exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) hxy' ha hb hab

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasDerivAtFilter.sum (h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) x L) :
    HasDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
L : Filter 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) x L
⊢ HasDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L

Tactic:
simpa [ContinuousLinearMap.sum_apply] using (HasFDerivAtFilter.sum h).hasDerivAtFilter

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_zero_left : logb 0 x = 0

Proof state:
x : ℝ
⊢ logb 0 x = 0

Tactic:
simp only [← log_div_log, log_zero, div_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem inter' (i : Fin N.succ) : dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Proof state:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
I : i = last N
this : 0 ≤ a.r (last N)
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
simp only [I, add_nonneg this this, dist_self]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
I : i = last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
have := (a.rpos (last N)).le

Result:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
I : i = last N
this : 0 ≤ a.r (last N)
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Proof state:
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
rcases lt_or_le i (last N) with (H | H)

Result:
case inl
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : i < last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Proof state:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
have I : i = last N := top_le_iff.1 H

Result:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
I : i = last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Proof state:
case inl
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : i < last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
exact a.inter i H

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma H1Cotangent.equivOfFormallySmooth_toLinearMap {P₁ P₂ : Extension R S} (f : P₁.Hom P₂)
    [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] :
    (H1Cotangent.equivOfFormallySmooth P₁ P₂).toLinearMap = map f

Proof state:
case h
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ ↑(equivOfFormallySmooth P₁ P₂) x = (map f) x

Tactic:
refine (LinearEquiv.symm_apply_eq _).mpr ?_

Result:
case h
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ ↑((LinearEquiv.ofBijective (map P₁.toInfinitesimal) ⋯).trans
          (equiv (P₁.homInfinitesimal P₂) (P₂.homInfinitesimal P₁)))
      x =
    (LinearEquiv.ofBijective (map P₂.toInfinitesimal) ⋯) ((map f) x)

Proof state:
case h
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (↑S (map (P₁.homInfinitesimal P₂)) ∘ₗ map P₁.toInfinitesimal) x = (↑S (map P₂.toInfinitesimal) ∘ₗ map f) x

Tactic:
rw [← map_comp, ← map_comp, map_eq]

Result:
no goals

Proof state:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
⊢ ↑(equivOfFormallySmooth P₁ P₂) = map f

Tactic:
ext1 x

Result:
case h
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ ↑(equivOfFormallySmooth P₁ P₂) x = (map f) x

Proof state:
case h
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ ↑((LinearEquiv.ofBijective (map P₁.toInfinitesimal) ⋯).trans
          (equiv (P₁.homInfinitesimal P₂) (P₂.homInfinitesimal P₁)))
      x =
    (LinearEquiv.ofBijective (map P₂.toInfinitesimal) ⋯) ((map f) x)

Tactic:
show ((map (P₁.homInfinitesimal P₂)).restrictScalars S ∘ₗ map P₁.toInfinitesimal) x =
  ((map P₂.toInfinitesimal).restrictScalars S ∘ₗ map f) x

Result:
case h
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (↑S (map (P₁.homInfinitesimal P₂)) ∘ₗ map P₁.toInfinitesimal) x = (↑S (map P₂.toInfinitesimal) ∘ₗ map f) x
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem dist_le_of_approx_trajectories_ODE_of_mem
    (hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t))
    (hf : ContinuousOn f (Icc a b))
    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t)
    (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf)
    (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
    (hg : ContinuousOn g (Icc a b))
    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t)
    (g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg)
    (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
    (ha : dist (f a) (g a) ≤ δ) :
    ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ K (εf + εg) (t - a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
⊢ ∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K) (εf + εg) (t - a)

Tactic:
apply norm_le_gronwallBound_of_norm_deriv_right_le (hf.sub hg) h_deriv ha

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
⊢ ∀ x ∈ Ico a b, ‖f' x - g' x‖ ≤ ↑K * ‖f x - g x‖ + (εf + εg)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forIn'_toList [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as.toList → β → m (ForInStep β)) :
    forIn' as.toList b f = forIn' as b (fun a m b => f a (mem_toList.mpr m) b)

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ }.toList → β → m (ForInStep β)
⊢ forIn' { toList := toList✝ }.toList b f = forIn' { toList := toList✝ } b fun a m b => f a ⋯ b

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as : Array α
b : β
f : (a : α) → a ∈ as.toList → β → m (ForInStep β)
⊢ forIn' as.toList b f = forIn' as b fun a m b => f a ⋯ b

Tactic:
cases as

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ }.toList → β → m (ForInStep β)
⊢ forIn' { toList := toList✝ }.toList b f = forIn' { toList := toList✝ } b fun a m b => f a ⋯ b
-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma t1_comp_t1_neg (c : k) : (T1 f c).comp (T1 f (-c)) = AlgHom.id _ _

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (T1 f c).comp (T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
rw [comp_aeval, ← MvPolynomial.aeval_X_left]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (MvPolynomial.aeval fun i =>
      (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i)) =
    MvPolynomial.aeval MvPolynomial.X

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (MvPolynomial.aeval fun i =>
      (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i)) =
    MvPolynomial.aeval MvPolynomial.X

Tactic:
ext i v

Result:
case hf.a
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
i : Fin (n + 1)
v : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.coeff v
      ((MvPolynomial.aeval fun i =>
          (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i))
        (MvPolynomial.X i)) =
    MvPolynomial.coeff v ((MvPolynomial.aeval MvPolynomial.X) (MvPolynomial.X i))

Proof state:
case hf.a
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
i : Fin (n + 1)
v : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.coeff v
      ((MvPolynomial.aeval fun i =>
          (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i))
        (MvPolynomial.X i)) =
    MvPolynomial.coeff v ((MvPolynomial.aeval MvPolynomial.X) (MvPolynomial.X i))

Tactic:
cases i using Fin.cases <;>
simp [Fin.succ_ne_zero]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem WellFoundedGT.finite_of_sSupIndep [WellFoundedGT α] {s : Set α}
    (hs : sSupIndep s) : s.Finite

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ False

Tactic:
replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t := by
  have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
  obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
  exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩

Result:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
⊢ False
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem _root_.MeasureTheory.StronglyMeasurable.integral_condDistrib (hf : StronglyMeasurable f) :
    StronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂condDistrib Y X μ x)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x

Tactic:
exact hf.integral_kernel_prod_right'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : Ω), f (x, y) ∂(condDistrib Y X μ) x

Tactic:
rw [condDistrib]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem normalClosure_le_normal {N : Subgroup G} [N.Normal] (h : s ⊆ N) : normalClosure s ≤ N

Proof state:
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ a ∈ N

Tactic:
refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N

case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Proof state:
case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

Tactic:
exact mul_mem ihx ihy

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
⊢ normalClosure s ≤ N

Tactic:
intro a w

Result:
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ a ∈ N

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

Tactic:
exact conjugatesOfSet_subset h hx

Result:
no goals

Proof state:
case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
exact inv_mem ihx

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N

Tactic:
exact one_mem _

Result:
no goals
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
theorem contMDiffOn_comp_diffeomorph_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : N → M'} {s} (hm : m ≤ n) :
    ContMDiffOn I I' m (f ∘ h) s ↔ ContMDiffOn J I' m f (h.symm ⁻¹' s) :=
  h.toEquiv.forall_congr fun {_} => by
    simp only [hm, coe_toEquiv, h.symm_apply_apply, contMDiffWithinAt_comp_diffeomorph_iff,
      mem_preimage]

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : WithTop ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
hm : m ≤ n
x✝ : M
⊢ x✝ ∈ s → ContMDiffWithinAt I I' m (f ∘ ⇑h) s x✝ ↔
    h.toEquiv x✝ ∈ ⇑h.symm ⁻¹' s → ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h.toEquiv x✝)

Tactic:
simp only [hm, coe_toEquiv, h.symm_apply_apply, contMDiffWithinAt_comp_diffeomorph_iff,
  mem_preimage]

Result:
no goals
-- Mathlib/Algebra/Algebra/Hom.lean
lemma algebraMapSubmonoid_le_comap (f : A →ₐ[R] B) :
    algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (algebraMapSubmonoid B M)

Tactic:
rw [← algebraMapSubmonoid_map_eq M f]

Result:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Submonoid.map f (algebraMapSubmonoid A M))

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Submonoid.map f (algebraMapSubmonoid A M))

Tactic:
exact Submonoid.le_comap_map (Algebra.algebraMapSubmonoid A M)

Result:
no goals