harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
lemma NonUnitalSubalgebra.toSubalgebra_toNonUnitalSubalgebra (S : NonUnitalSubalgebra R A)
    (h1 : (1 : A) ∈ S) : (NonUnitalSubalgebra.toSubalgebra S h1).toNonUnitalSubalgebra = S

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toSubalgebra h1).toNonUnitalSubalgebra = S

Tactic:
cases S

Result:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }

Proof state:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
theorem cardPowDegree_anti_archimedean {x y z : Fq[X]} {a : ℤ} (hxy : cardPowDegree (x - y) < a)
    (hyz : cardPowDegree (y - z) < a) : cardPowDegree (x - z) < a

Proof state:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
⊢ cardPowDegree (x - z) < a

Tactic:
by_cases hxy' : x = y

Result:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x = y
⊢ cardPowDegree (x - z) < a

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
⊢ cardPowDegree (x - z) < a

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ (x - z).degree ≤ (x - y).degree ⊔ (y - z).degree

Tactic:
convert degree_add_le (x - y) (y - z) using 2

Result:
case h.e'_3.h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ x - z = x - y + (y - z)

Proof state:
case h.e'_3.h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ x - z = x - y + (y - z)

Tactic:
exact (sub_add_sub_cancel _ _ _).symm

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_two_eq_two_mod (n : ℕ) : (2 : ZMod n).val = 2 % n

Proof state:
n : ℕ
⊢ val 2 = 2 % n

Tactic:
rw [← Nat.cast_two, val_natCast]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem LowerSemicontinuousWithinAt.add' {f g : α → γ} (hf : LowerSemicontinuousWithinAt f s x)
    (hg : LowerSemicontinuousWithinAt g s x)
    (hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
    LowerSemicontinuousWithinAt (fun z => f z + g z) s x

Proof state:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
H : ¬g z ≤ g x
⊢ g z ⊓ g x ∈ v

Tactic:
simpa [le_of_not_le H] using h₂ ⟨z₂lt, le_rfl⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem chaar_mem_clPrehaar (K₀ : PositiveCompacts G) (V : OpenNhdsOf (1 : G)) :
    chaar K₀ ∈ clPrehaar (K₀ : Set G) V

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this : ∀ (i : OpenNhdsOf 1), Classical.choose ⋯ ∈ clPrehaar (↑K₀) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V

Tactic:
exact this V

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this : Classical.choose ⋯ ∈ ⋂ V, clPrehaar (↑K₀) V
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V

Tactic:
rw [mem_iInter] at this

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this : ∀ (i : OpenNhdsOf 1), Classical.choose ⋯ ∈ clPrehaar (↑K₀) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V

Tactic:
have := (Classical.choose_spec (nonempty_iInter_clPrehaar K₀)).2

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this : Classical.choose ⋯ ∈ ⋂ V, clPrehaar (↑K₀) V
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma norm_cfcHom (a : A) (f : C(σ 𝕜 a, 𝕜)) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
f : C(↑(σ 𝕜 a), 𝕜)
ha : autoParam (p a) _auto✝
⊢ ‖(cfcHom ⋯) f‖ = ‖f‖

Tactic:
refine isometry_cfcHom a |>.norm_map_of_map_zero (map_zero _) f

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem LinearMap.quasiMeasurePreserving (f : E →ₗ[ℝ] E) (hf : LinearMap.det f ≠ 0) :
    QuasiMeasurePreserving f μ μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ map (⇑f) μ ≪ μ

Tactic:
rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ ≪ μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ QuasiMeasurePreserving (⇑f) μ μ

Tactic:
refine ⟨f.continuous_of_finiteDimensional.measurable, ?_⟩

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ map (⇑f) μ ≪ μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ ≪ μ

Tactic:
exact smul_absolutelyContinuous

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_map_left (m : γ → β → δ) (n : α → γ) :
    map₂ m (f.map n) g = map₂ (fun a b => m (n a) b) f g

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map ((fun p => m p.1 p.2) ∘ fun p => (n p.1, id p.2)) (f ×ˢ g) = map (fun p => m (n p.1) p.2) (f ×ˢ g)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map₂ m (map n f) g = map₂ (fun a b => m (n a) b) f g

Tactic:
rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, map_id]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map ((fun p => m p.1 p.2) ∘ fun p => (n p.1, id p.2)) (f ×ˢ g) = map (fun p => m (n p.1) p.2) (f ×ˢ g)
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem lt_translationNumber_of_forall_add_lt (hf : Continuous f) {z : ℝ} (hz : ∀ x, x + z < f x) :
    z < τ f

Proof state:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ z < τ f

Tactic:
refine lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) ?_

Result:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ f x - x ≤ τ f

Proof state:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ ∀ (x_1 : ℝ), f x - x ≤ f x_1 - x_1

Tactic:
exact f.forall_map_sub_of_Icc _ hx

Result:
no goals

Proof state:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ ∀ (x_1 : ℝ), x_1 + (f x - x) ≤ f x_1

Tactic:
simp only [← le_sub_iff_add_le']

Result:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ ∀ (x_1 : ℝ), f x - x ≤ f x_1 - x_1

Proof state:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ f x - x ≤ τ f

Tactic:
apply le_translationNumber_of_add_le

Result:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ ∀ (x_1 : ℝ), x_1 + (f x - x) ≤ f x_1

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
⊢ z < τ f

Tactic:
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y :=
  isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn

Result:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ z < τ f
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma oddKernel_neg (a : UnitAddCircle) (x : ℝ) : oddKernel (-a) x = -oddKernel a x

Proof state:
a : UnitAddCircle
x : ℝ
⊢ oddKernel (-a) x = -oddKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
| H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, oddKernel_def, jacobiTheta₂''_neg_left]

Result:
no goals

Proof state:
case H
x a : ℝ
⊢ oddKernel (-↑a) x = -oddKernel (↑a) x

Tactic:
simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, oddKernel_def, jacobiTheta₂''_neg_left]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem update_eq_single_add_erase (f : α →₀ M) (a : α) (b : M) :
    f.update a b = single a b + f.erase a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ f.update a b = single a b + erase a f

Tactic:
ext j

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ (f.update a b) j = (single a b + erase a f) j

Proof state:
case h.inr
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ (f.update a b) j = (single a b + erase a f) j

Tactic:
simp [Function.update_of_ne h.symm, single_apply, h, erase_ne, h.symm]

Result:
no goals

Proof state:
case h.inl
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ (f.update a b) a = (single a b + erase a f) a

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ (f.update a b) j = (single a b + erase a f) j

Tactic:
rcases eq_or_ne a j with (rfl | h)

Result:
case h.inl
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ (f.update a b) a = (single a b + erase a f) a

case h.inr
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ (f.update a b) j = (single a b + erase a f) j
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem pi_eq_bot_iff (H : ∀ i, Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀ i, H i = ⊥

Proof state:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

Tactic:
simp only [eq_bot_iff_forall]

Result:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ x ∈ pi univ H, x = 1) ↔ ∀ (i : η), ∀ x ∈ H i, x = 1

Proof state:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ x ∈ pi univ H, x = 1
i : η
x : f i
hx : x ∈ H i
this : (MonoidHom.mulSingle f i) x = 1
⊢ x = 1

Tactic:
simpa using congr_fun this i

Result:
no goals

Proof state:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ x ∈ pi univ H, x = 1) → ∀ (i : η), ∀ x ∈ H i, x = 1

Tactic:
intro h i x hx

Result:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ x ∈ pi univ H, x = 1
i : η
x : f i
hx : x ∈ H i
⊢ x = 1

Proof state:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ x ∈ pi univ H, x = 1
i : η
x : f i
hx : x ∈ H i
⊢ x = 1

Tactic:
have : MonoidHom.mulSingle f i x = 1 :=
  h (MonoidHom.mulSingle f i x) ((mulSingle_mem_pi i x).mpr fun _ => hx)

Result:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ x ∈ pi univ H, x = 1
i : η
x : f i
hx : x ∈ H i
this : (MonoidHom.mulSingle f i) x = 1
⊢ x = 1

Proof state:
case mpr
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (i : η), ∀ x ∈ H i, x = 1) → ∀ x ∈ pi univ H, x = 1

Tactic:
exact fun h x hx => funext fun i => h _ _ (hx i trivial)

Result:
no goals

Proof state:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ x ∈ pi univ H, x = 1) ↔ ∀ (i : η), ∀ x ∈ H i, x = 1

Tactic:
constructor

Result:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ x ∈ pi univ H, x = 1) → ∀ (i : η), ∀ x ∈ H i, x = 1

case mpr
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (i : η), ∀ x ∈ H i, x = 1) → ∀ x ∈ pi univ H, x = 1
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem exists_measurable_superset_ae_eq (h : NullMeasurableSet s μ) :
    ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Tactic:
rcases h with ⟨t, htm, hst⟩

Result:
case intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Proof state:
case intro.intro.refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s

Tactic:
exact diff_subset_iff.1 (subset_toMeasurable _ _)

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ toMeasurable μ (s \ t) =ᶠ[ae μ] ∅

Tactic:
simp [ae_le_set.1 hst.le]

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Tactic:
refine ⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩

Result:
case intro.intro.refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s

case intro.intro.refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s

Proof state:
case intro.intro.refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
this : toMeasurable μ (s \ t) =ᶠ[ae μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s

Tactic:
simpa only [union_empty] using hst.symm.union this

Result:
no goals

Proof state:
case intro.intro.refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s

Tactic:
have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]

Result:
case intro.intro.refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
this : toMeasurable μ (s \ t) =ᶠ[ae μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s
-- Mathlib/Analysis/RCLike/Basic.lean
theorem normSq_add (z w : K) : normSq (z + w) = normSq z + normSq w + 2 * re (z * conj w)

Proof state:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z + re w) * (re z + re w) + (im z + im w) * (im z + im w) =
    re z * re z + im z * im z + (re w * re w + im w * im w) + 2 * (re z * re w - im z * -im w)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ normSq (z + w) = normSq z + normSq w + 2 * re (z * (starRingEnd K) w)

Tactic:
simp only [normSq_apply, map_add, rclike_simps]

Result:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z + re w) * (re z + re w) + (im z + im w) * (im z + im w) =
    re z * re z + im z * im z + (re w * re w + im w * im w) + 2 * (re z * re w - im z * -im w)
-- Mathlib/Data/Finsupp/Single.lean
theorem support_update_ne_zero [DecidableEq α] (h : b ≠ 0) :
    support (f.update a b) = insert a f.support

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (f.update a b).support = insert a f.support

Tactic:
classical
simp only [update, h, ite_false, mem_support_iff, ne_eq]
congr!

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (f.update a b).support = insert a f.support

Tactic:
simp only [update, h, ite_false, mem_support_iff, ne_eq]

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h : b ≠ 0
⊢ insert a f.support = insert a f.support

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h : b ≠ 0
⊢ insert a f.support = insert a f.support

Tactic:
congr!

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
lemma TensorProduct.equivFinsuppOfBasisLeft_symm :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.toLinearMap =
    Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N) (ℬ i)

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
⊢ ↑(equivFinsuppOfBasisLeft ℬ).symm = (Finsupp.lsum R) fun i => (mk R M N) (ℬ i)

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
a✝ : ι
x✝ : N
⊢ (↑(equivFinsuppOfBasisLeft ℬ).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i => (mk R M N) (ℬ i)) ∘ₗ Finsupp.lsingle a✝) x✝

Proof state:
case h.h
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
a✝ : ι
x✝ : N
⊢ (↑(equivFinsuppOfBasisLeft ℬ).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i => (mk R M N) (ℬ i)) ∘ₗ Finsupp.lsingle a✝) x✝

Tactic:
simp [equivFinsuppOfBasisLeft]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_Δ : (W.map φ).Δ = φ W.Δ

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ -φ W.b₂ ^ 2 * φ W.b₈ - 8 * φ W.b₄ ^ 3 - 27 * φ W.b₆ ^ 2 + 9 * φ W.b₂ * φ W.b₄ * φ W.b₆ =
    φ (-W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).Δ = φ W.Δ

Tactic:
simp only [Δ, map_b₂, map_b₄, map_b₆, map_b₈]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ -φ W.b₂ ^ 2 * φ W.b₈ - 8 * φ W.b₄ ^ 3 - 27 * φ W.b₆ ^ 2 + 9 * φ W.b₂ * φ W.b₄ * φ W.b₆ =
    φ (-W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆)
-- Mathlib/Data/Nat/PartENat.lean
theorem ne_top_iff {x : PartENat} : x ≠ ⊤ ↔ ∃ n : ℕ, x = n

Proof state:
x : PartENat
⊢ x ≠ ⊤ ↔ ∃ n, x = ↑n

Tactic:
simpa only [← some_eq_natCast] using Part.ne_none_iff

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
theorem X_pow_sub_C_irreducible_of_prime_pow
    {p : ℕ} (hp : p.Prime) (hp' : p ≠ 2) (n : ℕ) {a : K} (ha : ∀ b : K, b ^ p ≠ a) :
    Irreducible (X ^ (p ^ n) - C a)

Proof state:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ n
⊢ ∀ (b : K), b ^ q ≠ a

Tactic:
simpa [(Nat.prime_dvd_prime_iff_eq hq hp).mp (hq.dvd_of_dvd_pow hq')] using ha

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p ^ n → ∀ (b : K), b ^ p_1 ≠ a

Tactic:
intros q hq hq'

Result:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ n
⊢ ∀ (b : K), b ^ q ≠ a

Proof state:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ p ^ n - C a)

Tactic:
apply X_pow_sub_C_irreducible_of_odd (hp.odd_of_ne_two hp').pow

Result:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p ^ n → ∀ (b : K), b ^ p_1 ≠ a
-- Mathlib/Data/Matroid/Closure.lean
lemma mem_closure_diff_singleton_iff_closure (he : e ∈ X) (heE : e ∈ M.E

Proof state:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ X
heE : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X

Tactic:
simpa using subset_closure_diff_iff_closure_eq (Y := {e}) (X := X) (by simpa)

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ X
heE : autoParam (e ∈ M.E) _auto✝
⊢ {e} ⊆ X

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem lt_trans {f g h : CauSeq α abs} (fg : f < g) (gh : g < h) : f < h :=
  show Pos (h - f) by
    convert add_pos fg gh using 1
    simp

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ (h - f).Pos

Tactic:
convert add_pos fg gh using 1

Result:
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ h - f = g - f + (h - g)

Proof state:
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ h - f = g - f + (h - g)

Tactic:
simp

Result:
no goals