harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_preΨ' (n : ℕ) : (W.map f).preΨ' n = (W.preΨ' n).map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℕ
⊢ (W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)

Tactic:
simp only [preΨ', map_Ψ₂Sq, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_preNormEDS']

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℕ
⊢ preNormEDS' ((mapRingHom f) W.Ψ₂Sq ^ 2) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n =
    preNormEDS' ((mapRingHom f) (W.Ψ₂Sq ^ 2)) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℕ
⊢ preNormEDS' ((mapRingHom f) W.Ψ₂Sq ^ 2) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n =
    preNormEDS' ((mapRingHom f) (W.Ψ₂Sq ^ 2)) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n

Tactic:
map_simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_eq (f : α → E) : ⨍ x, f x ∂μ = (μ univ).toReal⁻¹ • ∫ x, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
⊢ ⨍ (x : α), f x ∂μ = (μ univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rw [average_eq', integral_smul_measure, ENNReal.toReal_inv]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_iUnionLift [Countable ι] {t : ι → Set α} {f : ∀ i, t i → β}
    (htf : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩)
    {T : Set α} (hT : T ⊆ ⋃ i, t i) (htm : ∀ i, MeasurableSet (t i)) (hfm : ∀ i, Measurable (f i)) :
    Measurable (iUnionLift t f htf T hT) := fun s hs => by
  rw [preimage_iUnionLift]
  exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)

Tactic:
rw [preimage_iUnionLift]

Result:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (inclusion hT ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' s))

Proof state:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (inclusion hT ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' s))

Tactic:
exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
theorem riemannZeta_eulerProduct_hasProd (hs : 1 < s.re) :
    HasProd (fun p : Primes ↦ (1 - (p : ℂ) ^ (-s))⁻¹) (riemannZeta s)

Proof state:
s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p => (1 - ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n)

Tactic:
apply eulerProduct_completely_multiplicative_hasProd <| summable_riemannZetaSummand hs

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p => (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)

Tactic:
rw [← tsum_riemannZetaSummand hs]

Result:
s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p => (1 - ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n)
-- Mathlib/Algebra/CharP/Defs.lean
lemma false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharP R 1
⊢ False

Tactic:
have : Subsingleton R := CharOne.subsingleton

Result:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharP R 1
this : Subsingleton R
⊢ False

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharP R 1
this : Subsingleton R
⊢ False

Tactic:
exact false_of_nontrivial_of_subsingleton R

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem preimage_empty : r.preimage ∅ = ∅

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r.preimage ∅ = ∅

Tactic:
rw [preimage, image_empty]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffOn_of_subsingleton [Subsingleton F] : ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffOn 𝕜 n (fun x => 0) s

Tactic:
exact contDiffOn_const

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffOn 𝕜 n f s

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffOn 𝕜 n (fun x => 0) s
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem sSup {ℐ : Set (Ideal A)} (h : ∀ I ∈ ℐ, Ideal.IsHomogeneous 𝒜 I) :
    (sSup ℐ).IsHomogeneous 𝒜

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (SupSet.sSup ℐ)

Tactic:
rw [sSup_eq_iSup]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)

Tactic:
exact iSup₂ h

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma π_comp_map : solution.π.comp relations.map = 0

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.π ∘ₗ relations.map = 0

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem diff_erase (l₁ l₂ : List α) (a : α) : (l₁.diff l₂).erase a = (l₁.erase a).diff l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (l₁.diff l₂).erase a = (l₁.erase a).diff l₂

Tactic:
rw [← diff_cons_right, diff_cons]

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ n` is integrable for all nonnegative `p : ℝ`. -/
lemma integrable_rpow_abs_of_mem_interior_integrableExpSet
    (h : 0 ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ |X ω| ^ p) μ

Proof state:
case h.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ (fun ω => |X ω| ^ p) = fun ω => |X ω| ^ p * rexp (0 * X ω)

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => |X ω| ^ p) μ

Tactic:
convert integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet h hp using 1

Result:
case h.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ (fun ω => |X ω| ^ p) = fun ω => |X ω| ^ p * rexp (0 * X ω)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem enum_append (xs ys : List α) : enum (xs ++ ys) = enum xs ++ enumFrom xs.length ys

Proof state:
α : Type u_1
xs ys : List α
⊢ (xs ++ ys).enum = xs.enum ++ enumFrom xs.length ys

Tactic:
simp [enum, enumFrom_append]

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
lemma rangeLiftInclusion : (liftInclusion S).toHom.range = ⨆ i, S i

Proof state:
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
⊢ (liftInclusion S).toHom.range = ⨆ i, S i

Tactic:
simp_rw [liftInclusion, range_lift, Substructure.range_subtype]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem _root_.MeasurableEmbedding.memLp_map_measure_iff {g : β → F} (hf : MeasurableEmbedding f) :
    MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
⊢ MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Tactic:
simp_rw [MemLp, hf.aestronglyMeasurable_map_iff, hf.eLpNorm_map_measure]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem typein_le_typein' (o : Ordinal) {x y : o.toType} :
    typein (α := o.toType) (· < ·) x ≤ typein (α := o.toType) (· < ·) y ↔ x ≤ y

Proof state:
o : Ordinal.{u_1}
x y : o.toType
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding x ≤ (typein fun x1 x2 => x1 < x2).toRelEmbedding y ↔ x ≤ y

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem mem_segment_sub_add [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x - y -[𝕜] x + y]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x ∈ [x - y-[𝕜]x + y]

Tactic:
convert @midpoint_mem_segment 𝕜 _ _ _ _ _ (x - y) (x + y)

Result:
case h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)

Proof state:
case h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)

Tactic:
rw [midpoint_sub_add]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
theorem generateFrom_eq_prod {C : Set (Set α)} {D : Set (Set β)} (hC : generateFrom C = ‹_›)
    (hD : generateFrom D = ‹_›) (h2C : IsCountablySpanning C) (h2D : IsCountablySpanning D) :
    generateFrom (image2 (· ×ˢ ·) C D) = Prod.instMeasurableSpace

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst✝¹
hD : generateFrom D = inst✝
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
⊢ generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) C D) = Prod.instMeasurableSpace

Tactic:
rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive Bornology.IsBounded.exists_pos_norm_lt]
lemma Bornology.IsBounded.exists_pos_norm_lt' (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R :=
  let ⟨R, hR₀, hR⟩ := hs.exists_pos_norm_le'
  ⟨R + 1, by positivity, fun x hx ↦ (hR x hx).trans_lt (lt_add_one _)⟩

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R : ℝ
hR₀ : R > 0
hR : ∀ x ∈ s, ‖x‖ ≤ R
⊢ R + 1 > 0

Tactic:
positivity

Result:
no goals
-- Mathlib/Order/Antichain.lean
theorem subsingleton [IsTrichotomous α r] (h : IsAntichain r s) : s.Subsingleton

Proof state:
case inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

Tactic:
exact h.eq ha hb hab

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

Tactic:
exact hab

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b

Tactic:
exact h.eq' ha hb hab

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
⊢ s.Subsingleton

Tactic:
rintro a ha b hb

Result:
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b

Tactic:
obtain hab | hab | hab := trichotomous_of r a b

Result:
case inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

case inr.inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExpKernel_comp_trim (hm : m ≤ mΩ) : condExpKernel μ m ∘ₘ μ.trim hm = μ

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ ⇑(condExpKernel μ m) ∘ₘ μ.trim hm = μ

Tactic:
rw [← Measure.snd_compProd, compProd_trim_condExpKernel, @Measure.snd_map_prod_mk, Measure.map_id]

Result:
case hX
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ Measurable id

Proof state:
case hX
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ Measurable id

Tactic:
exact measurable_id'' hm

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
theorem AutGalois.π_surjective (A : PointedGaloisObject F) :
    Function.Surjective (AutGalois.π F A) := fun (σ : Aut A.obj) ↦ by
  have (i : PointedGaloisObject F) : Finite ((autGaloisSystem F ⋙ forget _).obj i) :=
    inferInstanceAs <| Finite (Aut (i.obj))
  exact eval_section_surjective_of_surjective
    (autGaloisSystem F ⋙ forget _) (autGaloisSystem_map_surjective F) A σ

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
A : PointedGaloisObject F
σ : Aut A.obj
this : ∀ (i : PointedGaloisObject F), Finite ((autGaloisSystem F ⋙ forget Grp).obj i)
⊢ ∃ a, (π F A) a = σ

Tactic:
exact eval_section_surjective_of_surjective
  (autGaloisSystem F ⋙ forget _) (autGaloisSystem_map_surjective F) A σ

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
A : PointedGaloisObject F
σ : Aut A.obj
⊢ ∃ a, (π F A) a = σ

Tactic:
have (i : PointedGaloisObject F) : Finite ((autGaloisSystem F ⋙ forget _).obj i) :=
  inferInstanceAs <| Finite (Aut (i.obj))

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
A : PointedGaloisObject F
σ : Aut A.obj
this : ∀ (i : PointedGaloisObject F), Finite ((autGaloisSystem F ⋙ forget Grp).obj i)
⊢ ∃ a, (π F A) a = σ
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem yz_succ_succ (n) : yz a1 (n + 2) = (2 * a : ℕ) * yz a1 (n + 1) - yz a1 n :=
  eq_sub_of_add_eq <| by delta yz; rw [← Int.ofNat_add, ← Int.ofNat_mul, yn_succ_succ]

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yz a1 (n + 2) + yz a1 n = ↑(2 * a) * yz a1 (n + 1)

Tactic:
delta yz

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(yn a1 (n + 2)) + ↑(yn a1 n) = ↑(2 * a) * ↑(yn a1 (n + 1))

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(yn a1 (n + 2)) + ↑(yn a1 n) = ↑(2 * a) * ↑(yn a1 (n + 1))

Tactic:
rw [← Int.ofNat_add, ← Int.ofNat_mul, yn_succ_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_add_left {a b : Nat} : max a (b + a) = b + a

Proof state:
a b : Nat
⊢ max a (b + a) = b + a

Tactic:
rw [Nat.max_def]

Result:
a b : Nat
⊢ (if a ≤ b + a then b + a else a) = b + a

Proof state:
a b : Nat
⊢ (if a ≤ b + a then b + a else a) = b + a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_eq_U_comp_half_mul_X [Invertible (2 : R)] (n : ℤ) :
    S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (fun x => x.comp (Polynomial.C ⅟2 * X)) ((S R n).comp (2 * X)) = (fun x => x.comp (Polynomial.C ⅟2 * X)) (U R n)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul,
  Nat.cast_ofNat, mul_invOf_self', map_one, one_mul, comp_X] at this

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : S R n = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : S R n = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
assumption

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₆_of_char_two : W.b₆ = W.a₃ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₃ ^ 2 + 4 * W.a₆ = W.a₃ ^ 2

Tactic:
linear_combination 2 * W.a₆ * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.b₆ = W.a₃ ^ 2

Tactic:
rw [b₆]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₃ ^ 2 + 4 * W.a₆ = W.a₃ ^ 2
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma rootSpace_zsmul_add_ne_bot_iff_mem (hα : α.IsNonZero) (n : ℤ) :
    rootSpace H (n • α + β) ≠ ⊥ ↔ n ∈ Finset.Icc (-chainBotCoeff α β : ℤ) (chainTopCoeff α β)

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ∈ Finset.Icc (-↑(chainBotCoeff (⇑α) β)) ↑(chainTopCoeff (⇑α) β)

Tactic:
rw [rootSpace_zsmul_add_ne_bot_iff α β hα n, Finset.mem_Icc, and_comm, neg_le]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_polynomialX :
    (W'.map f).toProjective.polynomialX = MvPolynomial.map f W'.polynomialX

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toProjective.polynomialX = (MvPolynomial.map f) W'.polynomialX

Tactic:
simp only [polynomialX, map_polynomial, pderiv_map]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
/-- Elements in `M ⊗ N` can be represented by sum of elements in `M` tensor elements of basis of
`N`. -/
lemma TensorProduct.eq_repr_basis_right :
    ∃ b : κ →₀ M, b.sum (fun i m ↦ m ⊗ₜ 𝒞 i) = x

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ b, (b.sum fun i m => m ⊗ₜ[R] 𝒞 i) = x

Tactic:
simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ b, (b.sum fun i m => m ⊗ₜ[R] 𝒞 i) = x

Tactic:
classical simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem epi_snd_of_isLimit [Epi f] {s : PullbackCone f g} (hs : IsLimit s) : Epi s.snd

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
⊢ Epi s.snd

Tactic:
haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.right) :=
  Abelian.epi_pullback_of_epi_f f g

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)
⊢ Epi s.snd

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)
⊢ Epi s.snd

Tactic:
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
@[simp] lemma prob_compl_eq_zero_iff₀ (hs : NullMeasurableSet s μ) : μ sᶜ = 0 ↔ μ s = 1

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ μ sᶜ = 0 ↔ μ s = 1

Tactic:
rw [prob_compl_eq_one_sub₀ hs, tsub_eq_zero_iff_le, one_le_prob_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
@[simp] lemma mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b

Proof state:
a : ℤ
ha : 0 ≤ a
b : ℕ
⊢ 0 ≤ mkRat a b

Tactic:
simpa using divInt_nonneg ha (Int.natCast_nonneg _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_neg_eq_log (x : ℝ) : log (-x) = log x

Proof state:
x : ℝ
⊢ log (-x) = log x

Tactic:
rw [← log_abs x, ← log_abs (-x), abs_neg]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_left_inj [IsLeftCancelAdd α] (hx : x ≠ ⊥) : x + y = x + z ↔ y = z

Proof state:
case intro
α : Type u
inst✝¹ : Add α
y z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Add α
x y z : WithBot α
inst✝ : IsLeftCancelAdd α
hx : x ≠ ⊥
⊢ x + y = x + z ↔ y = z

Tactic:
lift x to α using hx

Result:
case intro
α : Type u
inst✝¹ : Add α
y z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z