harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Substructures.lean
theorem range_subtype (S : L.Substructure M) : S.subtype.toHom.range = S

Proof state:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S

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

Result:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S

Proof state:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ x ∈ S.subtype.toHom.range ↔ x ∈ S

Tactic:
simp only [Hom.mem_range, Embedding.coe_toHom, coe_subtype]

Result:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.subtype.toHom.range = S

Tactic:
ext x

Result:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ x ∈ S.subtype.toHom.range ↔ x ∈ S

Proof state:
case h.intro.mk
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
y : M
hy : y ∈ S
⊢ ↑⟨y, hy⟩ ∈ S

Tactic:
exact hy

Result:
no goals

Proof state:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S

Tactic:
rintro ⟨⟨y, hy⟩, rfl⟩

Result:
case h.intro.mk
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
y : M
hy : y ∈ S
⊢ ↑⟨y, hy⟩ ∈ S
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_lt_iff_one_lt_mul : a⁻¹ < b ↔ 1 < b * a :=
  (mul_lt_mul_iff_right a).symm.trans <| by rw [inv_mul_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a⁻¹ * a < b * a ↔ 1 < b * a

Tactic:
rw [inv_mul_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
@[simp, measurability]
protected lemma MeasurableSet.himp {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
    MeasurableSet (s₁ ⇨ s₂)

Proof state:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)

Tactic:
exact h₂.union h₁.compl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ⇨ s₂)

Tactic:
rw [himp_eq]

Result:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem pred_eq_iff_not_succ' {o} : pred o = o ↔ ∀ a, o ≠ succ a

Proof state:
o : Ordinal.{u_4}
⊢ o.pred = o ↔ ∀ (a : Ordinal.{u_4}), o ≠ succ a

Tactic:
simpa using pred_eq_iff_not_succ

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_equation (hf : Function.Injective f) (P : Fin 3 → R) :
    (W'.map f).toProjective.Equation (f ∘ P) ↔ W'.Equation P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (map W' f).toProjective.Equation (⇑f ∘ P) ↔ W'.Equation P

Tactic:
simp only [Equation, map_polynomial, eval_map, ← eval₂_comp, map_eq_zero_iff f hf]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
theorem norm_normedMk_le : ‖normedMk (M := M)‖ ≤ 1 :=
  NormedAddGroupHom.opNorm_le_bound _ zero_le_one fun m => by simp

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
m : M
⊢ ‖normedMk m‖ ≤ 1 * ‖m‖

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk_cancel_common_left (s' s : S) (m : M) : mk (s' • m) (s' * s) = mk m s :=
  mk_eq.mpr
    ⟨1, by
      simp only [mul_smul, one_smul]
      rw [smul_comm]⟩

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s' s : ↥S
m : M
⊢ 1 • s • s' • m = 1 • (s' * s) • m

Tactic:
simp only [mul_smul, one_smul]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s' s : ↥S
m : M
⊢ s • s' • m = s' • s • m

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s' s : ↥S
m : M
⊢ s • s' • m = s' • s • m

Tactic:
rw [smul_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem ofScientific_false_def : Rat.ofScientific m false e = (m * 10 ^ e : Nat)

Proof state:
m e : Nat
⊢ Rat.ofScientific m false e = ↑(m * 10 ^ e)

Tactic:
unfold Rat.ofScientific

Result:
m e : Nat
⊢ (if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)) = ↑(m * 10 ^ e)

Proof state:
m e : Nat
⊢ (if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)) = ↑(m * 10 ^ e)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem add_zero [NeZero n] (k : Fin n) : k + 0 = k

Proof state:
n : Nat
inst✝ : NeZero n
k : Fin n
⊢ k + 0 = k

Tactic:
ext

Result:
case h
n : Nat
inst✝ : NeZero n
k : Fin n
⊢ ↑(k + 0) = ↑k

Proof state:
case h
n : Nat
inst✝ : NeZero n
k : Fin n
⊢ ↑(k + 0) = ↑k

Tactic:
simp [add_def, Nat.mod_eq_of_lt k.2]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Defs.lean
theorem subsingleton_iff : Subsingleton (M ⧸ p) ↔ ∀ x : M, x ∈ p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (a : M), mk a = 0) ↔ ∀ (x : M), x ∈ p

Tactic:
simp_rw [Submodule.Quotient.mk_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton (M ⧸ p) ↔ ∀ (x : M), x ∈ p

Tactic:
rw [subsingleton_iff_forall_eq 0, Submodule.Quotient.forall]

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (a : M), mk a = 0) ↔ ∀ (x : M), x ∈ p
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem polarCoord_symm_apply (p : ℝ × ℝ) :
    Complex.polarCoord.symm p = p.1 * (Real.cos p.2 + Real.sin p.2 * Complex.I)

Proof state:
p : ℝ × ℝ
⊢ ↑Complex.polarCoord.symm p = ↑p.1 * (↑(Real.cos p.2) + ↑(Real.sin p.2) * I)

Tactic:
simp [Complex.polarCoord, equivRealProdCLM_symm_apply, mul_add, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
protected lemma sq_eq_sq_iff_eq_or_eq_neg (h : Commute a b) : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Proof state:
R : Type u
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Tactic:
rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
/-- See `le_expGrowthSup_mul'` for a version with swapped argument `u` and `v`. -/
lemma le_expGrowthSup_mul {u v : ℕ → ℝ≥0∞} :
    expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)

Tactic:
refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Result:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n = ((u * v) n).log / ↑n

Proof state:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n = ((u * v) n).log / ↑n

Tactic:
rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem haveLebesgueDecomposition_mk (μ : Measure α) {f : α → ℝ} (hf : Measurable f)
    (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
    s.HaveLebesgueDecomposition μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ s.HaveLebesgueDecomposition μ

Tactic:
exact haveLebesgueDecomposition_mk' μ hf hfi htμ hadd

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ

Tactic:
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd

Result:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ

Tactic:
refine haveLebesgueDecomposition_mk' μ measurable_zero (integrable_zero _ _ μ) htμ ?_

Result:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t + μ.withDensityᵥ 0

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t + μ.withDensityᵥ 0

Tactic:
rwa [withDensityᵥ_zero, add_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ s.HaveLebesgueDecomposition μ

Tactic:
by_cases hfi : Integrable f μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ s.HaveLebesgueDecomposition μ

case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ
-- Mathlib/Data/List/EditDistance/Bounds.lean
theorem le_levenshtein_cons (xs : List α) (y ys) :
    ∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys ≤ levenshtein C xs (y :: ys)

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
⊢ ∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys ≤ levenshtein C xs (y :: ys)

Tactic:
simpa [suffixLevenshtein_eq_tails_map, List.minimum_le_coe_iff] using
  suffixLevenshtein_minimum_le_levenshtein_cons (δ := δ) xs y ys

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem evariance_mul (c : ℝ) (X : Ω → ℝ) (μ : Measure Ω) :
    evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * evariance X μ

Proof state:
case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ ^ 2 = ENNReal.ofReal (c ^ 2) * ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2

Tactic:
rw [integral_mul_left, ← mul_sub, enorm_mul, mul_pow, ← enorm_pow,
  Real.enorm_of_nonneg (sq_nonneg _)]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ eVar[fun ω => c * X ω; μ] = ENNReal.ofReal (c ^ 2) * eVar[X; μ]

Tactic:
rw [evariance, evariance, ← lintegral_const_mul' _ _ ENNReal.ofReal_lt_top.ne]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ ∫⁻ (ω : Ω), ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ ^ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (c ^ 2) * ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ ∫⁻ (ω : Ω), ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ ^ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (c ^ 2) * ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ

Tactic:
congr with ω

Result:
case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ ^ 2 = ENNReal.ofReal (c ^ 2) * ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_le_of_brange_subset {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal}
    (h : brange o f ⊆ brange o' g) : bsup.{u, max v w} o f ≤ bsup.{v, max u w} o' g :=
  bsup_le fun i hi => by
    obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, rfl⟩
    rw [← hj']
    apply le_bsup

Proof state:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ o'.bsup g

Tactic:
apply le_bsup

Result:
no goals

Proof state:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ o'.bsup g

Tactic:
obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, rfl⟩

Result:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ o'.bsup g

Proof state:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ o'.bsup g

Tactic:
rw [← hj']

Result:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ o'.bsup g
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signAux_one (n : ℕ) : signAux (1 : Perm (Fin n)) = 1

Proof state:
n : ℕ
⊢ (∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = 1

Tactic:
conv => rhs; rw [← @Finset.prod_const_one _ _ (finPairsLT n)]

Result:
n : ℕ
⊢ (∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = ∏ _x ∈ finPairsLT n, 1

Proof state:
n : ℕ
⊢ signAux 1 = 1

Tactic:
unfold signAux

Result:
n : ℕ
⊢ (∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = 1

Proof state:
n : ℕ
⊢ (∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = ∏ _x ∈ finPairsLT n, 1

Tactic:
exact Finset.prod_congr rfl fun a ha => if_neg (mem_finPairsLT.1 ha).not_le

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coe_injective : Function.Injective (Coe.coe : MvPolynomial σ R → MvPowerSeries σ R) :=
    fun x y h => by
  ext
  simp_rw [← coeff_coe]
  congr

Proof state:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R m✝) ↑x = (MvPowerSeries.coeff R m✝) ↑y

Tactic:
congr

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
⊢ x = y

Tactic:
ext

Result:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y

Proof state:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y

Tactic:
simp_rw [← coeff_coe]

Result:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R m✝) ↑x = (MvPowerSeries.coeff R m✝) ↑y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getD_getElem? (a : Vector α n) (i : Nat) (d : α) :
    a[i]?.getD d = if p : i < n then a[i]'p else d

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
d : α
h : i < n
⊢ a[i]?.getD d = if p : i < n then a[i] else d

Tactic:
simp [h, getElem?_def]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
d : α
h : ¬i < n
⊢ a[i]?.getD d = if p : i < n then a[i] else d

Tactic:
have p : i ≥ n := Nat.le_of_not_gt h

Result:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
d : α
h : ¬i < n
p : i ≥ n
⊢ a[i]?.getD d = if p : i < n then a[i] else d

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
d : α
⊢ a[i]?.getD d = if p : i < n then a[i] else d

Tactic:
if h : i < n then
  simp [h, getElem?_def]
else
  have p : i ≥ n := Nat.le_of_not_gt h
  simp [getElem?_eq_none p, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
d : α
h : ¬i < n
p : i ≥ n
⊢ a[i]?.getD d = if p : i < n then a[i] else d

Tactic:
simp [getElem?_eq_none p, h]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is monotone when `t ≠ ∞`. -/
lemma monotone_truncateToReal {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) : Monotone (truncateToReal t)

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ t.truncateToReal x ≤ t.truncateToReal y

Tactic:
simp only [truncateToReal]

Result:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ (t ⊓ x).toReal ≤ (t ⊓ y).toReal

Proof state:
case hb
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ t ⊓ y ≠ ⊤

Tactic:
exact ne_top_of_le_ne_top t_ne_top (min_le_left _ _)

Result:
no goals

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ (t ⊓ x).toReal ≤ (t ⊓ y).toReal

Tactic:
gcongr

Result:
case hb
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ t ⊓ y ≠ ⊤

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
⊢ Monotone t.truncateToReal

Tactic:
intro x y x_le_y

Result:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ t.truncateToReal x ≤ t.truncateToReal y
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem ContinuousMap.algHom_ext_map_X {A : Type*} [Ring A]
    [Algebra ℝ A] [TopologicalSpace A] [T2Space A] {s : Set ℝ} [CompactSpace s]
    {φ ψ : C(s, ℝ) →ₐ[ℝ] A} (hφ : Continuous φ) (hψ : Continuous ψ)
    (h : φ (toContinuousMapOnAlgHom s X) = ψ (toContinuousMapOnAlgHom s X)) : φ = ψ

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ (polynomialFunctions s).topologicalClosure ≤ AlgHom.equalizer φ ψ

Tactic:
exact Subalgebra.topologicalClosure_minimal (polynomialFunctions s)
  (polynomialFunctions.le_equalizer s φ ψ h) (isClosed_eq hφ hψ)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ φ = ψ

Tactic:
suffices (⊤ : Subalgebra ℝ C(s, ℝ)) ≤ AlgHom.equalizer φ ψ from
  AlgHom.ext fun x => this (by trivial)

Result:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ ⊤ ≤ AlgHom.equalizer φ ψ

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
this : ⊤ ≤ AlgHom.equalizer φ ψ
x : C(↑s, ℝ)
⊢ x ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ ⊤ ≤ AlgHom.equalizer φ ψ

Tactic:
rw [← polynomialFunctions.topologicalClosure s]

Result:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ (polynomialFunctions s).topologicalClosure ≤ AlgHom.equalizer φ ψ
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- See `MulAction.isBlock_subgroup'` for a version that works for the right action of a group on
itself. -/
@[to_additive "See `AddAction.isBlock_subgroup'` for a version that works for the right action
of a group on itself."]
lemma isBlock_subgroup : IsBlock G (s : Set H)

Proof state:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
⊢ ∀ ⦃g₁ g₂ : G⦄, g₁ • ↑s ≠ g₂ • ↑s → ∀ ⦃a : H⦄, a ∈ g₁ • ↑s → a ∉ g₂ • ↑s

Tactic:
rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s

Tactic:
rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
⊢ IsBlock G ↑s

Tactic:
simp only [IsBlock, disjoint_left]

Result:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
⊢ ∀ ⦃g₁ g₂ : G⦄, g₁ • ↑s ≠ g₂ • ↑s → ∀ ⦃a : H⦄, a ∈ g₁ • ↑s → a ∉ g₂ • ↑s

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False

Tactic:
refine hab ?_

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s
-- Mathlib/LinearAlgebra/QuadraticForm/Basis.lean
theorem toBilin_apply (Q : QuadraticMap R M N) (bm : Basis ι R M) (i j : ι) :
    Q.toBilin bm (bm i) (bm j) =
      if i = j then Q (bm i) else if i < j then polar Q (bm i) (bm j) else 0

Proof state:
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
i j : ι
⊢ ((Q.toBilin bm) (bm i)) (bm j) = if i = j then Q (bm i) else if i < j then polar (⇑Q) (bm i) (bm j) else 0

Tactic:
simp [toBilin]

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem Duplicate.mem_cons_self (h : x ∈+ x :: l) : x ∈ l

Proof state:
case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l

Tactic:
exact h.mem

Result:
no goals

Proof state:
α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l

Tactic:
obtain h | h := h

Result:
case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l

case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l

Proof state:
case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l

Tactic:
exact h

Result:
no goals