harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/AList.lean
theorem lookup_to_alist {a} (s : List (Sigma β)) : lookup a s.toAList = s.dlookup a

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a s.toAList = dlookup a s

Tactic:
rw [List.toAList, lookup, dlookup_dedupKeys]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
protected lemma _root_.MeasurableSet.everywherePosSubset [OpensMeasurableSpace α]
    (hs : MeasurableSet s) :
    MeasurableSet (μ.everywherePosSubset s)

Proof state:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (μ.everywherePosSubset s)

Tactic:
rw [hu]

Result:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (s \ u)

Proof state:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (s \ u)

Tactic:
exact hs.diff u_open.measurableSet

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : OpensMeasurableSpace α
hs : MeasurableSet s
⊢ MeasurableSet (μ.everywherePosSubset s)

Tactic:
rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩

Result:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (μ.everywherePosSubset s)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_zero_iff_sameRay {x y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ 0 ≤ (↑(inner x y) + (o.areaForm x) y • I).re ∧ (↑(inner x y) + (o.areaForm x) y • I).im = 0 ↔ SameRay ℝ x y

Tactic:
simpa using o.nonneg_inner_and_areaForm_eq_zero_iff_sameRay x y

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y = 0 ↔ SameRay ℝ x y

Tactic:
rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero,
  Complex.arg_eq_zero_iff]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ 0 ≤ (↑(inner x y) + (o.areaForm x) y • I).re ∧ (↑(inner x y) + (o.areaForm x) y • I).im = 0 ↔ SameRay ℝ x y
-- Mathlib/Data/Nat/Nth.lean
theorem image_nth_Iio_card (hf : (setOf p).Finite) : nth p '' Set.Iio #hf.toFinset = setOf p :=
  calc
    nth p '' Set.Iio #hf.toFinset = Set.range (hf.toFinset.orderEmbOfFin rfl)

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
⊢ nth p '' Set.Iio #hf.toFinset = Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)

Tactic:
ext x

Result:
case h
p : ℕ → Prop
hf : (setOf p).Finite
x : ℕ
⊢ x ∈ nth p '' Set.Iio #hf.toFinset ↔ x ∈ Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)

Proof state:
case h
p : ℕ → Prop
hf : (setOf p).Finite
x : ℕ
⊢ x ∈ nth p '' Set.Iio #hf.toFinset ↔ x ∈ Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)

Tactic:
simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf,
  Set.mem_Iio, exists_prop]

Result:
no goals

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
⊢ Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯) = setOf p

Tactic:
rw [range_orderEmbOfFin, Set.Finite.coe_toFinset]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma overGrothendieckTopology_eq_toGrothendieck_overPretopology :
    S.overGrothendieckTopology P = (S.overPretopology P).toGrothendieck

Proof state:
case h.h.h.mp.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Tactic:
letI (i : 𝒰.J) : (𝒰.obj i).Over S := { hom := 𝒰.map i ≫ X.hom }

Result:
case h.h.h.mp.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
this : (i : 𝒰.J) → (𝒰.obj i).Over S := fun i => { hom := 𝒰.map i ≫ X.hom }
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Proof state:
case h.h.h.mpr.intro.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
hT : 𝒰.toPresieveOver ≤ R.arrows
⊢ ∃ R_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows

Tactic:
use Presieve.ofArrows 𝒰.obj 𝒰.map, ⟨𝒰, rfl⟩

Result:
case right
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
hT : 𝒰.toPresieveOver ≤ R.arrows
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isNat_intCast {R} [Ring R] (n : ℤ) (m : ℕ) :
    IsNat n m → IsNat (n : R) m

Proof state:
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ ↑↑m = ↑m

Tactic:
simp

Result:
no goals

Proof state:
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m

Tactic:
exact ⟨by simp⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ IsNat n m → IsNat (↑n) m

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m
-- Mathlib/Analysis/RCLike/Basic.lean
theorem conj_ofReal (r : ℝ) : conj (r : K) = (r : K)

Proof state:
K : Type u_1
inst✝ : RCLike K
r : ℝ
⊢ (starRingEnd K) ↑r = ↑r

Tactic:
rw [ext_iff]

Result:
K : Type u_1
inst✝ : RCLike K
r : ℝ
⊢ re ((starRingEnd K) ↑r) = re ↑r ∧ im ((starRingEnd K) ↑r) = im ↑r

Proof state:
K : Type u_1
inst✝ : RCLike K
r : ℝ
⊢ re ((starRingEnd K) ↑r) = re ↑r ∧ im ((starRingEnd K) ↑r) = im ↑r

Tactic:
simp only [ofReal_im, conj_im, eq_self_iff_true, conj_re, and_self_iff, neg_zero]

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
lemma compProd_map_condDistrib (hY : AEMeasurable Y μ) :
    (μ.map X) ⊗ₘ condDistrib Y X μ = μ.map fun a ↦ (X a, Y a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hY : AEMeasurable Y μ
⊢ Measure.map X μ ⊗ₘ condDistrib Y X μ = Measure.map (fun a => (X a, Y a)) μ

Tactic:
rw [condDistrib, ← Measure.fst_map_prod_mk₀ hY, Measure.disintegrate]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma C_addPolynomial (x y L : R) : mk W (C <| W.addPolynomial x y L) =
    mk W ((Y - C (linePolynomial x y L)) * (W.negPolynomial - C (linePolynomial x y L))) :=
  AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [W.C_addPolynomial, add_sub_cancel_left, mul_one]⟩

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ C (W.addPolynomial x y L) - (Y - C (linePolynomial x y L)) * (W.negPolynomial - C (linePolynomial x y L)) =
    W.polynomial * 1

Tactic:
rw [W.C_addPolynomial, add_sub_cancel_left, mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem apply_le_mass (μ : FiniteMeasure Ω) (s : Set Ω) : μ s ≤ μ.mass

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
⊢ μ s ≤ μ.mass

Tactic:
simpa using apply_mono μ (subset_univ s)

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem inf_map {X Y : C} (g : Y ⟶ X) [Mono g] (f₁ f₂) :
    (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))

Tactic:
rw [pullback_comp, pullback_map_self]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

Tactic:
apply Quotient.ind'

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map g).obj f₂

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₁ f₂ : Subobject Y
⊢ (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

Tactic:
revert f₁

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map g).obj f₂

Tactic:
intro f₁

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))

Tactic:
dsimp

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂

Tactic:
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← map_comp]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_const_lt_top [IsFiniteMeasure μ] (s : Set α) {c : ℝ≥0∞} (hc : c ≠ ∞) :
    ∫⁻ _ in s, c ∂μ < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c * (μ.restrict s) univ < ⊤

Tactic:
exact ENNReal.mul_lt_top hc.lt_top (measure_lt_top (μ.restrict s) univ)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ ∫⁻ (x : α) in s, c ∂μ < ⊤

Tactic:
rw [lintegral_const]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c * (μ.restrict s) univ < ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_consₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β)
    (h : Raw.WFImp m.1) (a : α) (b : β a) : IsHashSelf (m.consₘ a b).1.buckets

Proof state:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
⊢ containsKey ⟨a, b⟩.fst l.toList = true ∨ hash ⟨a, b⟩.fst = hash a

Tactic:
exact Or.inr rfl

Result:
no goals

Proof state:
case inr
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
exact Or.inl (containsKey_of_mem hp)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ IsHashSelf (m.consₘ a b).val.buckets

Tactic:
apply h.buckets_hash_self.updateBucket (fun l p hp => ?_)

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.cons a b l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.cons a b l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
simp only [AssocList.toList_cons, mem_cons] at hp

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p = ⟨a, b⟩ ∨ p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p = ⟨a, b⟩ ∨ p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
rcases hp with (rfl|hp)

Result:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
⊢ containsKey ⟨a, b⟩.fst l.toList = true ∨ hash ⟨a, b⟩.fst = hash a

case inr
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_one_of_subsingleton [Subsingleton α] (s : Set α) : s.ncard ≤ 1

Proof state:
α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ s.ncard ≤ 1

Tactic:
rw [ncard_eq_toFinset_card]

Result:
α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ ⋯.toFinset.card ≤ 1

Proof state:
α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ ⋯.toFinset.card ≤ 1

Tactic:
exact Finset.card_le_one_of_subsingleton _

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem inter_eq_singleton_orthogonalProjection {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) :
    (s : Set P) ∩ mk' p s.directionᗮ = {↑(orthogonalProjection s p)}

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑s ∩ ↑(mk' p s.directionᗮ) = {orthogonalProjectionFn s p}

Tactic:
exact inter_eq_singleton_orthogonalProjectionFn p

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑s ∩ ↑(mk' p s.directionᗮ) = {↑((orthogonalProjection s) p)}

Tactic:
rw [← orthogonalProjectionFn_eq]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑s ∩ ↑(mk' p s.directionᗮ) = {orthogonalProjectionFn s p}
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements less than something in `𝒜`.

See also `Finset.mem_shadow_iterate_iff_exists_sdiff`. -/
lemma mem_shadow_iterate_iff_exists_mem_card_add :
    t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + k

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + k

Tactic:
refine mem_shadow_iterate_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
  and_congr_right fun hst ↦ ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = k ↔ #t = #t✝ + k

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t

Tactic:
exact card_mono hst

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = k ↔ #t = #t✝ + k

Tactic:
rw [card_sdiff hst, tsub_eq_iff_eq_add_of_le, add_comm]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem liftR_map_last' [LawfulMvFunctor F] {α : TypeVec n} {ι} (R : ι → ι → Prop) (x : F (α ::: ι))
    (f : ι → ι) (hh : ∀ x : ι, R (f x) x) : LiftR' (RelLast' _ R) ((id ::: f) <$$> x) x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this : LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) ((TypeVec.id ::: _root_.id) <$$> x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x

Tactic:
rwa [appendFun_id_id, MvFunctor.id_map] at this

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x

Tactic:
have := liftR_map_last R x f id hh

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this : LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) ((TypeVec.id ::: _root_.id) <$$> x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_b₂ : (W.variableChange C).b₂ = C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) =
    ↑C.u⁻¹ ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂ + 12 * C.r)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (W.variableChange C).b₂ = ↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)

Tactic:
simp only [b₂, variableChange_a₁, variableChange_a₂]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) =
    ↑C.u⁻¹ ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂ + 12 * C.r)
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_eq {σ : Perm α} (l : List (Perm α)) (h0 : l.prod = σ)
    (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) :
    σ.cycleType = l.map (Finset.card ∘ support)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ Multiset.map (Finset.card ∘ support) l.toFinset.val = ↑(List.map (Finset.card ∘ support) l)

Tactic:
simp [List.dedup_eq_self.mpr hl, Function.comp_def]

Result:
no goals

Proof state:
case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ l.toFinset.noncommProd id ⋯ = σ

Tactic:
simp [hl, h0]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ σ.cycleType = ↑(List.map (Finset.card ∘ support) l)

Tactic:
rw [cycleType_eq' l.toFinset]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ Multiset.map (Finset.card ∘ support) l.toFinset.val = ↑(List.map (Finset.card ∘ support) l)

case h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ ∀ f ∈ l.toFinset, f.IsCycle

case h2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ (↑l.toFinset).Pairwise Disjoint

case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ l.toFinset.noncommProd id ⋯ = σ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
⊢ σ.cycleType = ↑(List.map (Finset.card ∘ support) l)

Tactic:
have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ σ.cycleType = ↑(List.map (Finset.card ∘ support) l)

Proof state:
case h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ ∀ f ∈ l.toFinset, f.IsCycle

Tactic:
simpa using h1

Result:
no goals

Proof state:
case h2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ (↑l.toFinset).Pairwise Disjoint

Tactic:
simpa [hl] using h2

Result:
no goals