harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem algebraMap_injective_of_field_isFractionRing (K L : Type*) [Field K] [Semiring L]
    [Nontrivial L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L]
    [IsScalarTower R S L] [IsScalarTower R K L] : Function.Injective (algebraMap R S)

Proof state:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑(algebraMap R S)

Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_

Result:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))

Proof state:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))

Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]

Result:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

Proof state:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem map_bijective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
    Bijective (map f g) ↔ Bijective f ∧ Bijective g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this✝ : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
exact (map_injective.and map_surjective).trans and_and_and_comm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
haveI := Nonempty.map f ‹_›

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
haveI := Nonempty.map g ‹_›

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this✝ : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
theorem mdifferentiableOn_extChartAt_symm :
    MDifferentiableOn 𝓘(𝕜, E) I (extChartAt I x).symm (extChartAt I x).target

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
⊢ MDifferentiableOn 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (extChartAt I x).target

Tactic:
intro y hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (extChartAt I x).target y

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (extChartAt I x).target y

Tactic:
exact (mdifferentiableWithinAt_extChartAt_symm hy).mono (extChartAt_target_subset_range x)

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_eq_diagonal_iff [Zero α] {d₁ d₂ : n → α} :
    diagonal d₁ = diagonal d₂ ↔ ∀ i, d₁ i = d₂ i :=
  ⟨fun h i => by simpa using congr_arg (fun m : Matrix n n α => m i i) h, fun h => by
    rw [show d₁ = d₂ from funext h]⟩

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i

Tactic:
simpa using congr_arg (fun m : Matrix n n α => m i i) h

Result:
no goals

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : ∀ (i : n), d₁ i = d₂ i
⊢ diagonal d₁ = diagonal d₂

Tactic:
rw [show d₁ = d₂ from funext h]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem leftRel_r_eq_leftCosetEquivalence :
    ⇑(QuotientGroup.leftRel s) = LeftCosetEquivalence s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ⇑(leftRel s) = LeftCosetEquivalence ↑s

Tactic:
ext

Result:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (leftRel s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝

Proof state:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝

Tactic:
exact (leftCoset_eq_iff s).symm

Result:
no goals

Proof state:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (leftRel s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝

Tactic:
rw [leftRel_eq]

Result:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@[simp]
lemma toNNReal_neg_algebraMap (r : ℝ≥0) : (- algebraMap ℝ C(X, ℝ) r).toNNReal = 0

Proof state:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑((-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(0 a✝)

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
⊢ (-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = 0

Tactic:
ext

Result:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑((-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(0 a✝)
-- Mathlib/Data/Set/Card.lean
theorem ncard_subtype (P : α → Prop) (s : Set α) :
    { x : Subtype P | (x : α) ∈ s }.ncard = (s ∩ setOf P).ncard

Proof state:
α : Type u_1
P : α → Prop
s : Set α
⊢ {x | ↑x ∈ s}.ncard = (s ∩ setOf P).ncard

Tactic:
convert (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm

Result:
case h.e'_3.h.e'_2
α : Type u_1
P : α → Prop
s : Set α
⊢ s ∩ setOf P = (fun a => ↑a) '' {x | ↑x ∈ s}

Proof state:
case h.e'_3.h.e'_2
α : Type u_1
P : α → Prop
s : Set α
⊢ s ∩ setOf P = (fun a => ↑a) '' {x | ↑x ∈ s}

Tactic:
ext x

Result:
case h.e'_3.h.e'_2.h
α : Type u_1
P : α → Prop
s : Set α
x : α
⊢ x ∈ s ∩ setOf P ↔ x ∈ (fun a => ↑a) '' {x | ↑x ∈ s}

Proof state:
case h.e'_3.h.e'_2.h
α : Type u_1
P : α → Prop
s : Set α
x : α
⊢ x ∈ s ∩ setOf P ↔ x ∈ (fun a => ↑a) '' {x | ↑x ∈ s}

Tactic:
simp [← and_assoc, exists_eq_right]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem totalDegree (hφ : IsHomogeneous φ n) (h : φ ≠ 0) : totalDegree φ = n

Proof state:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (weight 1) d ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x

Tactic:
simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]

Result:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun i c => c) ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x

Proof state:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ n ≤ φ.totalDegree

Tactic:
simp only [← hφ hd, MvPolynomial.totalDegree, Finsupp.sum]

Result:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x

Proof state:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun i c => c) ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x

Tactic:
exact Finset.le_sup (f := fun s ↦ ∑ x ∈ s.support, s x) hd

Result:
no goals

Proof state:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x

Tactic:
replace hd := Finsupp.mem_support_iff.mpr hd

Result:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (weight 1) d ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ n ≤ φ.totalDegree

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h

Result:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ n ≤ φ.totalDegree

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ φ.totalDegree = n

Tactic:
apply le_antisymm hφ.totalDegree_le

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ n ≤ φ.totalDegree
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Ψ_one : W.Ψ 1 = 1

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ 1 = 1

Tactic:
rw [← Nat.cast_one, Ψ_ofNat, preΨ'_one, C_1, if_neg Nat.not_even_one, mul_one]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_le_comm : a \ b ≤ c ↔ a \ c ≤ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ≤ c ↔ a \ c ≤ b

Tactic:
rw [sdiff_le_iff, sdiff_le_iff']

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem HasDerivWithinAt.limsup_slope_norm_le (hf : HasDerivWithinAt f f' s x) (hr : ‖f'‖ < r) :
    ∀ᶠ z in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
apply (hf.limsup_norm_slope_le hr).mono

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ (x_1 : ℝ), ‖x_1 - x‖⁻¹ * ‖f x_1 - f x‖ < r → ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ 0 ≤ ‖z - x‖⁻¹

Tactic:
exact inv_nonneg.2 (norm_nonneg _)

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
refine lt_of_le_of_lt (mul_le_mul_of_nonneg_left (norm_sub_norm_le _ _) ?_) hz

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ 0 ≤ ‖z - x‖⁻¹

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ (x_1 : ℝ), ‖x_1 - x‖⁻¹ * ‖f x_1 - f x‖ < r → ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r

Tactic:
intro z hz

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_univ : (univ : Set α).WellFoundedOn r ↔ WellFounded r

Proof state:
α : Type u_2
r : α → α → Prop
⊢ univ.WellFoundedOn r ↔ WellFounded r

Tactic:
simp [wellFoundedOn_iff]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₂_app_two : (homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, by valid⟩ = app₂ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.177732, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
⊢ 2 < 2 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_add_subset [DecidableEq σ] (p q : MvPolynomial σ R) :
    (p + q).vars ⊆ p.vars ∪ q.vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p + q).vars ⊆ p.vars ∪ q.vars

Tactic:
intro x hx

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).vars
⊢ x ∈ p.vars ∪ q.vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).degrees
⊢ x ∈ p.degrees ∨ x ∈ q.degrees

Tactic:
simpa using Multiset.mem_of_le degrees_add_le hx

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).vars
⊢ x ∈ p.vars ∪ q.vars

Tactic:
simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx ⊢

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).degrees
⊢ x ∈ p.degrees ∨ x ∈ q.degrees
-- Mathlib/RingTheory/AlgebraTower.lean
theorem linearIndependent_smul {ι : Type*} {b : ι → S} {ι' : Type*} {c : ι' → A}
    (hb : LinearIndependent R b) (hc : LinearIndependent S c) :
    LinearIndependent R fun p : ι × ι' ↦ b p.1 • c p.2

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ LinearIndependent R fun p => b p.1 • c p.2

Tactic:
rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
  LinearIndependent, linearCombination_smul]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ Function.Injective
    ⇑(↑R (linearCombination S c) ∘ₗ mapRange.linearMap (linearCombination R b) ∘ₗ ↑(finsuppProdLEquiv R))

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ Function.Injective
    ⇑(↑R (linearCombination S c) ∘ₗ mapRange.linearMap (linearCombination R b) ∘ₗ ↑(finsuppProdLEquiv R))

Tactic:
simpa using Function.Injective.comp hc
  ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem not_IntegrableOn_Ici_inv {a : ℝ} :
    ¬ IntegrableOn (fun x => x⁻¹) (Ici a)

Proof state:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x
B : Tendsto (fun x => ‖Real.log x‖) atTop atTop
⊢ ¬IntegrableOn (fun x => x⁻¹) (Ici a) volume

Tactic:
exact not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter atTop (Ici_mem_atTop a)
  (A.mono (fun x hx ↦ hx.differentiableAt)) B
  (Filter.EventuallyEq.isBigO (A.mono (fun x hx ↦ hx.deriv)))

Result:
no goals

Proof state:
a : ℝ
⊢ ¬IntegrableOn (fun x => x⁻¹) (Ici a) volume

Tactic:
have A : ∀ᶠ x in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x := by
  filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)

Result:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x
⊢ ¬IntegrableOn (fun x => x⁻¹) (Ici a) volume

Proof state:
a : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x

Tactic:
filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)

Result:
no goals

Proof state:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x
⊢ ¬IntegrableOn (fun x => x⁻¹) (Ici a) volume

Tactic:
have B : Tendsto (fun x => ‖Real.log x‖) atTop atTop :=
  tendsto_norm_atTop_atTop.comp Real.tendsto_log_atTop

Result:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x
B : Tendsto (fun x => ‖Real.log x‖) atTop atTop
⊢ ¬IntegrableOn (fun x => x⁻¹) (Ici a) volume
-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
@[local simp]
lemma ae_toFiniteAux [SFinite μ] : ae μ.toFiniteAux = ae μ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : ¬IsFiniteMeasure μ
⊢ ae ⋯.choose = ae μ

Tactic:
obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec

Result:
case neg.intro.intro
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : ¬IsFiniteMeasure μ
left✝ : IsFiniteMeasure ⋯.choose
h₁ : μ ≪ ⋯.choose
h₂ : ⋯.choose ≪ μ
⊢ ae ⋯.choose = ae μ

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : IsFiniteMeasure μ
⊢ ae μ = ae μ

Tactic:
simp

Result:
no goals

Proof state:
case neg.intro.intro
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : ¬IsFiniteMeasure μ
left✝ : IsFiniteMeasure ⋯.choose
h₁ : μ ≪ ⋯.choose
h₂ : ⋯.choose ≪ μ
⊢ ae ⋯.choose = ae μ

Tactic:
exact h₂.ae_le.antisymm h₁.ae_le

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ae (if IsFiniteMeasure μ then μ else ⋯.choose) = ae μ

Tactic:
split_ifs

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : IsFiniteMeasure μ
⊢ ae μ = ae μ

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : ¬IsFiniteMeasure μ
⊢ ae ⋯.choose = ae μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ae μ.toFiniteAux = ae μ

Tactic:
rw [Measure.toFiniteAux]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ae (if IsFiniteMeasure μ then μ else ⋯.choose) = ae μ
-- Mathlib/ModelTheory/Order.lean
theorem realize_noBotOrder_iff : M ⊨ L.noBotOrderSentence ↔ NoBotOrder M

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ NoBotOrder M →
    ∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)

Tactic:
intro h a

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoBotOrder M
a : M
⊢ ∃ a_1,
    ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.noBotOrderSentence ↔ NoBotOrder M

Tactic:
simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
  BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize, Term.realize_le,
  Sum.elim_inr]

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ (∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)) ↔
    NoBotOrder M

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ (∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)) ↔
    NoBotOrder M

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

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ NoBotOrder M →
    ∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoBotOrder M
a : M
⊢ ∃ a_1,
    ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)

Tactic:
exact exists_not_ge a

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem liftOn_toFinmap {γ} (s : AList β) (f : AList β → γ) (H) : liftOn ⟦s⟧ f H = f s

Proof state:
case mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧.liftOn f H = f { entries := entries✝, nodupKeys := nodupKeys✝ }

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ ⟦s⟧.liftOn f H = f s

Tactic:
cases s

Result:
case mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧.liftOn f H = f { entries := entries✝, nodupKeys := nodupKeys✝ }