harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Adjoin/FG.lean
theorem fg_of_fg_map (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective f)
    (hs : (S.map f).FG) : S.FG :=
  let ⟨s, hs⟩ := hs
  ⟨s.preimage f fun _ _ _ _ h ↦ hf h,
    map_injective hf <| by
      rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]
      rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]
      exact map_mono le_top⟩

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f (Algebra.adjoin R ↑(s.preimage ⇑f ⋯)) = map f S

Tactic:
rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]

Result:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ⇑f

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ map f ⊤

Tactic:
exact map_mono le_top

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ⇑f

Tactic:
rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]

Result:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ map f ⊤
-- Mathlib/Data/Finset/Insert.lean
theorem mem_insert_coe {s : Finset α} {x y : α} : x ∈ insert y s ↔ x ∈ insert y (s : Set α)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
⊢ x ∈ insert y s ↔ x ∈ insert y ↑s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma comp_apply {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) :
    (f ≫ g) x = g (f x)

Proof state:
M N T : MonCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem exp_pow_eq_rescale_exp [Algebra ℚ A] (k : ℕ) : exp A ^ k = rescale (k : A) (exp A)

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
⊢ exp A ^ k = (rescale ↑k) (exp A)

Tactic:
induction' k with k h

Result:
case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A ^ 0 = (rescale ↑0) (exp A)

case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = (rescale ↑k) (exp A)
⊢ exp A ^ (k + 1) = (rescale ↑(k + 1)) (exp A)

Proof state:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = (rescale ↑k) (exp A)
⊢ exp A ^ (k + 1) = (rescale ↑(k + 1)) (exp A)

Tactic:
simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
id_apply, rescale_one] using pow_succ (exp A) k

Result:
no goals

Proof state:
case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A ^ 0 = (rescale ↑0) (exp A)

Tactic:
simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero, zero_eq,
  pow_zero (exp A), coe_comp]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sUnion_empty : ⋃₀ (∅ : Class.{u}) = (∅ : Class.{u})

Proof state:
⊢ ⋃₀ ∅ = ∅

Tactic:
ext

Result:
case a
z✝ : ZFSet.{u}
⊢ (⋃₀ ∅) z✝ ↔ ∅ z✝

Proof state:
case a
z✝ : ZFSet.{u}
⊢ (⋃₀ ∅) z✝ ↔ ∅ z✝

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma IsIntegralCurve.comp_mul (hγ : IsIntegralCurve γ v) (a : ℝ) :
    IsIntegralCurve (γ ∘ (· * a)) (a • v)

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsIntegralCurveOn γ v univ
a : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) univ

Tactic:
exact hγ.comp_mul _

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsIntegralCurve γ v
a : ℝ
⊢ IsIntegralCurve (γ ∘ fun x => x * a) (a • v)

Tactic:
rw [isIntegralCurve_iff_isIntegralCurveOn] at *

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsIntegralCurveOn γ v univ
a : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) univ
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_comp [DecidableEq γ] (f : γ → β) (g : α → γ) :
    ∏ a ∈ s, f (g a) = ∏ b ∈ s.image g, f b ^ #{a ∈ s | g a = b}

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
⊢ ∏ a ∈ s, f (g a) = ∏ b ∈ image g s, f b ^ #(filter (fun a => g a = b) s)

Tactic:
simp_rw [← prod_const, prod_fiberwise_of_maps_to' fun _ ↦ mem_image_of_mem _]

Result:
no goals
-- Mathlib/Topology/Order/T5.lean
theorem ordConnectedComponent_mem_nhds : ordConnectedComponent s a ∈ 𝓝 a ↔ s ∈ 𝓝 a

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
⊢ s.ordConnectedComponent a ∈ 𝓝 a

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhds h with ⟨b, c, ha, ha', hs⟩

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
b c : X
ha : a ∈ Icc b c
ha' : Icc b c ∈ 𝓝 a
hs : Icc b c ⊆ s
⊢ s.ordConnectedComponent a ∈ 𝓝 a

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
b c : X
ha : a ∈ Icc b c
ha' : Icc b c ∈ 𝓝 a
hs : Icc b c ⊆ s
⊢ s.ordConnectedComponent a ∈ 𝓝 a

Tactic:
exact mem_of_superset ha' (subset_ordConnectedComponent ha hs)

Result:
no goals

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s : Set X
⊢ s.ordConnectedComponent a ∈ 𝓝 a ↔ s ∈ 𝓝 a

Tactic:
refine ⟨fun h => mem_of_superset h ordConnectedComponent_subset, fun h => ?_⟩

Result:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
⊢ s.ordConnectedComponent a ∈ 𝓝 a
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem iInf_span_singleton_natCast {R : Type*} [CommRing R] {ι : Type*} [Fintype ι]
    {I : ι → ℕ} (hI : Pairwise fun i j => (I i).Coprime (I j)) :
    ⨅ (i : ι), span {(I i : R)} = span {((∏ i : ι, I i : ℕ) : R)}

Proof state:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Fintype ι
I : ι → ℕ
hI : Pairwise fun i j => (I i).Coprime (I j)
⊢ ∀ (i j : ι), i ≠ j → IsCoprime ↑(I i) ↑(I j)

Tactic:
exact fun i j h ↦ (hI h).cast

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Fintype ι
I : ι → ℕ
hI : Pairwise fun i j => (I i).Coprime (I j)
⊢ ⨅ i, span {↑(I i)} = span {↑(∏ i : ι, I i)}

Tactic:
rw [iInf_span_singleton, Nat.cast_prod]

Result:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Fintype ι
I : ι → ℕ
hI : Pairwise fun i j => (I i).Coprime (I j)
⊢ ∀ (i j : ι), i ≠ j → IsCoprime ↑(I i) ↑(I j)
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1S_sub {T : Set α → E →L[ℝ] F} (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T) (f g : α →₁ₛ[μ] E) :
    setToL1S T (f - g) = setToL1S T f - setToL1S T g

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (f - g) = setToL1S T f - setToL1S T g

Tactic:
rw [sub_eq_add_neg, setToL1S_add T h_zero h_add, setToL1S_neg h_zero h_add, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem isSigmaCompact_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsSigmaCompact (h ⁻¹' s) ↔ IsSigmaCompact s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s

Tactic:
exact h.symm.isSigmaCompact_image

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h ⁻¹' s) ↔ IsSigmaCompact s

Tactic:
rw [← image_symm]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoin_finset_isCompactElement (S : Finset E) :
    IsCompactElement (adjoin F S : IntermediateField F E)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
⊢ IsCompactElement (S.sup fun a => F⟮a⟯)

Tactic:
exact isCompactElement_finsetSup S fun x _ => adjoin_simple_isCompactElement x

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
⊢ IsCompactElement (⨆ x ∈ ↑S, F⟮x⟯)

Tactic:
simp_rw [Finset.mem_coe, ← Finset.sup_eq_iSup]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
⊢ IsCompactElement (S.sup fun a => F⟮a⟯)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
⊢ IsCompactElement (adjoin F ↑S)

Tactic:
rw [← biSup_adjoin_simple]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
⊢ IsCompactElement (⨆ x ∈ ↑S, F⟮x⟯)
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem _root_.QuadraticMap.polarBilin_comp (Q : QuadraticMap R N' N) (f : M →ₗ[R] N') :
    polarBilin (Q.comp f) = LinearMap.compl₁₂ (polarBilin Q) f f :=
  LinearMap.ext₂ <| fun x y => by simp [polar]

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
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
Q : QuadraticMap R N' N
f : M →ₗ[R] N'
x y : M
⊢ ((Q.comp f).polarBilin x) y = ((compl₁₂ Q.polarBilin f f) x) y

Tactic:
simp [polar]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem countable_cover_nhdsWithin [SecondCountableTopology α] {f : α → Set α} {s : Set α}
    (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Proof state:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
refine ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩

Result:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
x : α
hx : x ∈ s
⊢ x ∈ ⋃ x ∈ Subtype.val '' t, f x

Proof state:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
x : α
hx : x ∈ s
htU : ∀ (x : ↑s), ↑x ∈ ⋃ i ∈ t, f ↑i
⊢ x ∈ ⋃ y ∈ t, f ↑y

Tactic:
exact htU ⟨x, hx⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
x : α
hx : x ∈ s
⊢ x ∈ ⋃ x ∈ Subtype.val '' t, f x

Tactic:
simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢

Result:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
x : α
hx : x ∈ s
htU : ∀ (x : ↑s), ↑x ∈ ⋃ i ∈ t, f ↑i
⊢ x ∈ ⋃ y ∈ t, f ↑y

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)

Result:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
rcases countable_cover_nhds this with ⟨t, htc, htU⟩

Result:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
/-- The angle ∠AAB at a point is always `π / 2`. -/
@[simp] lemma angle_self_left (p₀ p : P) : ∠ p₀ p₀ p = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₀ p : P
⊢ InnerProductGeometry.angle (p₀ -ᵥ p₀) (p -ᵥ p₀) = π / 2

Tactic:
rw [vsub_self]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₀ p : P
⊢ InnerProductGeometry.angle 0 (p -ᵥ p₀) = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₀ p : P
⊢ ∠ p₀ p₀ p = π / 2

Tactic:
unfold angle

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₀ p : P
⊢ InnerProductGeometry.angle (p₀ -ᵥ p₀) (p -ᵥ p₀) = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₀ p : P
⊢ InnerProductGeometry.angle 0 (p -ᵥ p₀) = π / 2

Tactic:
exact angle_zero_left _

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma codisjoint_zeroLocus {U : X.Opens}
    (s : Set Γ(X, U)) : Codisjoint (X.zeroLocus s) U

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ Codisjoint (X.zeroLocus s) ↑U

Tactic:
have (x : X) : ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U := fun _ _ h ↦ X.basicOpen_le _ h

Result:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
this : ∀ (x : ↑↑X.toPresheafedSpace), ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U
⊢ Codisjoint (X.zeroLocus s) ↑U

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
this : ∀ (x : ↑↑X.toPresheafedSpace), ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U
⊢ Codisjoint (X.zeroLocus s) ↑U

Tactic:
simpa [codisjoint_iff_le_sup, Set.ext_iff, or_iff_not_imp_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_mapIdx {l : List α} {f : Nat → α → β} {g : Nat → β → γ} :
    (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
f : Nat → α → β
g : Nat → β → γ
⊢ mapIdx g (mapIdx f l) = mapIdx (fun i => g i ∘ f i) l

Tactic:
simp [mapIdx_eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_sub_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
    n₁ /. d₁ - n₂ /. d₂ = (n₁ * d₂ - n₂ * d₁) /. (d₁ * d₂)

Proof state:
n₁ n₂ d₁ d₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ n₁ /. d₁ - n₂ /. d₂ = (n₁ * d₂ - n₂ * d₁) /. (d₁ * d₂)

Tactic:
simp only [Rat.sub_eq_add_neg, neg_divInt,
  divInt_add_divInt _ _ z₁ z₂, Int.neg_mul, Int.sub_eq_add_neg]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq {x y : F} (h : W.Nonsingular x y) :
    ClassGroup.mk (XYIdeal' <| nonsingular_neg h) * ClassGroup.mk (XYIdeal' h) = 1

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ ClassGroup.mk (XYIdeal' ⋯ * XYIdeal' h) = 1

Tactic:
exact
  (ClassGroup.mk_eq_one_of_coe_ideal <| by exact (FractionalIdeal.coeIdeal_mul ..).symm.trans <|
    FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr ⟨_, XClass_ne_zero W _, rfl⟩

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ ClassGroup.mk (XYIdeal' ⋯) * ClassGroup.mk (XYIdeal' h) = 1

Tactic:
rw [← _root_.map_mul]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ ClassGroup.mk (XYIdeal' ⋯ * XYIdeal' h) = 1

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ ↑(XYIdeal' ⋯ * XYIdeal' h) = ↑(span {XClass W ?m.509908})

Tactic:
exact (FractionalIdeal.coeIdeal_mul ..).symm.trans <|
FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_hom_inv (X : C) {Y Z : C} (f : Y ≅ Z) :
    X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (X ⊗ Y)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (X ⊗ Y)

Tactic:
rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
lemma Set.Infinite.exists_accPt_cofinite_inf_principal [CompactSpace X] (hs : s.Infinite) :
    ∃ x, AccPt x (cofinite ⊓ 𝓟 s)

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : CompactSpace X
hs : s.Infinite
⊢ ∃ x, AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
simpa only [mem_univ, true_and]
  using hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact isCompact_univ s.subset_univ

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma freeOn_not_isLoop (E : Set α) (e : α) : ¬ (freeOn E).IsLoop e

Proof state:
α : Type u_1
E : Set α
e : α
⊢ ¬(freeOn E).IsLoop e

Tactic:
simp [isLoop_iff]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_eq_one_iff_isFixedPt : minimalPeriod f x = 1 ↔ IsFixedPt f x

Proof state:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f^[1] x

Tactic:
refine Function.IsPeriodicPt.isFixedPt ?_

Result:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x

Proof state:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f x

case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Proof state:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f x

Tactic:
rw [← iterate_one f]

Result:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f^[1] x

Proof state:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x

Tactic:
rw [← h]

Result:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x

Proof state:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
exact isPeriodicPt_minimalPeriod f x

Result:
no goals

Proof state:
case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Tactic:
exact
  ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
    (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem graph_eq_range_prod : f.graph = range (LinearMap.id.prod f)

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
x : M × M₂
⊢ x ∈ f.graph ↔ x ∈ range (id.prod f)

Tactic:
exact ⟨fun hx => ⟨x.1, Prod.ext rfl hx.symm⟩, fun ⟨u, hu⟩ => hu ▸ rfl⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
⊢ f.graph = range (id.prod f)

Tactic:
ext x

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
x : M × M₂
⊢ x ∈ f.graph ↔ x ∈ range (id.prod f)
-- Mathlib/Topology/Category/LightProfinite/Extend.lean
theorem functorOp_final (hc : IsLimit c) [∀ i, Epi (c.π.app i)] : Final (functorOp c)

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : (functor c).Initial
⊢ (functorOp c).Final

Tactic:
have : ((StructuredArrow.toCostructuredArrow toLightProfinite c.pt)).IsEquivalence  :=
  (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence )

Result:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this✝ : (functor c).Initial
this : (StructuredArrow.toCostructuredArrow toLightProfinite c.pt).IsEquivalence
⊢ (functorOp c).Final

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functorOp c).Final

Tactic:
have := functor_initial c hc

Result:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : (functor c).Initial
⊢ (functorOp c).Final

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this✝ : (functor c).Initial
this : (StructuredArrow.toCostructuredArrow toLightProfinite c.pt).IsEquivalence
⊢ (functorOp c).Final

Tactic:
have : (functor c).rightOp.Final :=
  inferInstanceAs ((opOpEquivalence ℕ).inverse ⋙ (functor c).op).Final

Result:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this✝¹ : (functor c).Initial
this✝ : (StructuredArrow.toCostructuredArrow toLightProfinite c.pt).IsEquivalence
this : (functor c).rightOp.Final
⊢ (functorOp c).Final

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this✝¹ : (functor c).Initial
this✝ : (StructuredArrow.toCostructuredArrow toLightProfinite c.pt).IsEquivalence
this : (functor c).rightOp.Final
⊢ (functorOp c).Final

Tactic:
exact Functor.final_comp (functor c).rightOp _

Result:
no goals