harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/IsTensorProduct.lean
lemma IsBaseChange.of_equiv (e : S ⊗[R] M ≃ₗ[S] N) (he : ∀ x, e (1 ⊗ₜ x) = f x) :
    IsBaseChange S f

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
⊢ ∀ (x : S) (y : M),
    (LinearEquiv.restrictScalars R e) (x ⊗ₜ[R] y) = ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x) y

Tactic:
intro x y

Result:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
x : S
y : M
⊢ (LinearEquiv.restrictScalars R e) (x ⊗ₜ[R] y) = ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x) y

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
⊢ IsBaseChange S f

Tactic:
apply IsTensorProduct.of_equiv (e.restrictScalars R)

Result:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
⊢ ∀ (x : S) (y : M),
    (LinearEquiv.restrictScalars R e) (x ⊗ₜ[R] y) = ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x) y

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
x : S
y : M
⊢ x ⊗ₜ[R] y = x • 1 ⊗ₜ[R] y

Tactic:
simp [smul_tmul']

Result:
no goals

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
x : S
y : M
⊢ (LinearEquiv.restrictScalars R e) (x ⊗ₜ[R] y) = ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x) y

Tactic:
simp [show x ⊗ₜ[R] y = x • (1 ⊗ₜ[R] y) by simp [smul_tmul'], he]

Result:
no goals
-- Mathlib/Combinatorics/Hindman.lean
theorem FP.finset_prod {M} [CommMonoid M] (a : Stream' M) (s : Finset ℕ) (hs : s.Nonempty) :
    (s.prod fun i => a.get i) ∈ FP a

Proof state:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_le this

Result:
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
induction s using Finset.strongInduction with | H s ih => _

Result:
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_or' : (or o o').map f = (o.map f).or (o'.map f)

Proof state:
α✝¹ : Type u_1
o o' : Option α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ Option.map f (o.or o') = (Option.map f o).or (Option.map f o')

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSets.piiUnionInter_of_not_mem {π : ι → Set (Set Ω)} {a : ι} {S : Finset ι}
    (hp_ind : iIndepSets π κ μ) (haS : a ∉ S) :
    IndepSets (piiUnionInter π S) (π a) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n => if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
⊢ t2 = f a

Tactic:
simp [f]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : ↑s ⊆ ↑S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
rw [Finset.coe_subset] at hs_mem

Result:
case intro.intro.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n => if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_forall : ∀ n ∈ s, f n = ft1 n
⊢ t1 = ⋂ n ∈ s, f n

Tactic:
rw [ht1_eq]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n => if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_forall : ∀ n ∈ s, f n = ft1 n
⊢ ⋂ x ∈ s, ft1 x = ⋂ n ∈ s, f n
-- Mathlib/RingTheory/FinitePresentation.lean
theorem of_restrict_scalars_finitePresentation [Algebra A B] [IsScalarTower R A B]
    [FinitePresentation.{w₁, w₃} R B] [FiniteType R A] :
    FinitePresentation.{w₂, w₃} A B

Proof state:
case intro.intro.intro.intro.refine_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max 0 w₁) := MvPolynomial (Fin n) R
AX : Type (max 0 w₂) := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A ↑⊤

Tactic:
exact fun {x} => subset_adjoin ⟨⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiff.pow {f : E → 𝔸} (hf : ContDiff 𝕜 n f) : ∀ m : ℕ, ContDiff 𝕜 n fun x => f x ^ m
  | 0 => by simpa using contDiff_const
  | m + 1 => by simpa [pow_succ] using (hf.pow m).mul hf

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : WithTop ℕ∞
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiff 𝕜 n f
⊢ ContDiff 𝕜 n fun x => f x ^ 0

Tactic:
simpa using contDiff_const

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : WithTop ℕ∞
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiff 𝕜 n f
m : ℕ
⊢ ContDiff 𝕜 n fun x => f x ^ (m + 1)

Tactic:
simpa [pow_succ] using (hf.pow m).mul hf

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem morphismRestrict_app {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) :
    (f ∣_ U).app V = f.app (U.ι ''ᵁ V) ≫
        X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
have e : U.ι ⁻¹ᵁ (U.ι ''ᵁ V) = V :=
  Opens.ext (Set.preimage_image_eq _ Subtype.coe_injective)

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.desc_comp_inl_comp_inr {W X Y Z : C} [HasBinaryCoproduct W Y]
    [HasBinaryCoproduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) :
    coprod.desc (g ≫ coprod.inl) (g' ≫ coprod.inr) = coprod.map g g'

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ map g g' ≫ desc inl inr = map g g'

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ desc (g ≫ inl) (g' ≫ inr) = map g g'

Tactic:
rw [← coprod.map_desc]

Result:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ map g g' ≫ desc inl inr = map g g'
-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem LinearMap.continuous_of_finiteDimensional [T2Space E] [FiniteDimensional 𝕜 E]
    (f : E →ₗ[𝕜] F') : Continuous f

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
⊢ Continuous ⇑f

Tactic:
let b := Basis.ofVectorSpace 𝕜 E

Result:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
⊢ Continuous ⇑f

Proof state:
case h.e'_5.h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
x : E
⊢ f x = (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun) x

Tactic:
dsimp

Result:
case h.e'_5.h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
x : E
⊢ f x = f (b.equivFun.symm ⇑(b.repr x))
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem zeroLocus_singleton_mul (f g : A) :
    zeroLocus 𝒜 ({f * g} : Set A) = zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g} :=
  Set.ext fun x => by simpa using x.isPrime.mul_mem_iff_mem_or_mem

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f * g} ↔ x ∈ zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g}

Tactic:
simpa using x.isPrime.mul_mem_iff_mem_or_mem

Result:
no goals
-- Mathlib/Analysis/Convex/Hull.lean
theorem affineSpan_convexHull (s : Set E) : affineSpan 𝕜 (convexHull 𝕜 s) = affineSpan 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s

Tactic:
refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) ≤ affineSpan 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)

Tactic:
exact convexHull_subset_affineSpan s

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) ≤ affineSpan 𝕜 s

Tactic:
rw [affineSpan_le]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
@[simp high]
lemma toCLM_apply_single [DecidableEq n] {M : CStarMatrix m n A} {j : n} (a : A) :
    (toCLM M) (equiv _ |>.symm <| Pi.single j a) = (equiv _).symm (fun i => M i j * a)

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : DecidableEq n
M : CStarMatrix m n A
j : n
a : A
⊢ (toCLM M) ((equiv (n → A)).symm (Pi.single j a)) = (equiv (m → A)).symm fun i => M i j * a

Tactic:
ext

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : DecidableEq n
M : CStarMatrix m n A
j : n
a : A
i✝ : m
⊢ (toCLM M) ((equiv (n → A)).symm (Pi.single j a)) i✝ = (equiv (m → A)).symm (fun i => M i j * a) i✝

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : DecidableEq n
M : CStarMatrix m n A
j : n
a : A
i✝ : m
⊢ (toCLM M) ((equiv (n → A)).symm (Pi.single j a)) i✝ = (equiv (m → A)).symm (fun i => M i j * a) i✝

Tactic:
simp [toCLM_apply, EmbeddingLike.apply_eq_iff_eq, equiv, Equiv.refl]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem induced_topology_eq_preorder [Preorder α] [Preorder β] [TopologicalSpace β]
    [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y)
    (H₁ : ∀ {a b x}, b < f a → ¬(b < f x) → ∃ y, y < a ∧ b ≤ f y)
    (H₂ : ∀ {a b x}, f a < b → ¬(f x < b) → ∃ y, a < y ∧ f y ≤ b) :
    induced f ‹TopologicalSpace β› = Preorder.topology α

Proof state:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ = Preorder.topology α

Tactic:
have : OrderTopology α := ⟨rfl⟩

Result:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ = Preorder.topology α

Proof state:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤
    (⨅ i ∈ Iio (f a), 𝓟 (f ⁻¹' Ioi i)) ⊓ ⨅ i ∈ Ioi (f a), 𝓟 (f ⁻¹' Iio i)

Tactic:
refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)

Result:
case refine_1
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

case refine_2
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma limsup_add_le_of_le {a b : EReal} (ha : limsup u f < a) (hb : limsup v f ≤ b) :
    limsup (u + v) f ≤ a + b

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
⊢ limsup (u + v) f ≤ a + b

Tactic:
rcases eq_top_or_lt_top b with rfl | h

Result:
case inl
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ a + ⊤

case inr
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b

Proof state:
case inl
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b

Tactic:
exact (limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)

Result:
no goals

Proof state:
case inl
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ a + ⊤

Tactic:
rw [add_top_of_ne_bot ha.ne_bot]

Result:
case inl
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ ⊤
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.unique [Unique I] :
    OrthogonalIdempotents e ↔ IsIdempotentElem (e default)

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Unique I
⊢ OrthogonalIdempotents e ↔ IsIdempotentElem (e default)

Tactic:
simp only [orthogonalIdempotents_iff, Unique.forall_iff, Subsingleton.pairwise, and_true]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem appTop (H : P f) [IsAffine X] [IsAffine Y] : Q f.appTop.hom

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
rw [Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE]

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))

Tactic:
exact appLE P f H ⟨_, isAffineOpen_top _⟩ ⟨_, isAffineOpen_top _⟩ _

Result:
no goals