harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem sumInv_apply (x : AdicCompletion I (⨁ j, M j)) (j : ι) :
    (sumInv I M x) j = map I (component R ι _ j) x

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ ((sumInv I M) x) j = (map I (component R ι M j)) x

Tactic:
apply induction_on I _ x (fun x ↦ ?_)

Result:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x✝ : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence I (⨁ (j : ι), M j)
⊢ ((sumInv I M) ((mk I (⨁ (j : ι), M j)) x)) j = (map I (component R ι M j)) ((mk I (⨁ (j : ι), M j)) x)

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x✝ : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence I (⨁ (j : ι), M j)
⊢ ((sumInv I M) ((mk I (⨁ (j : ι), M j)) x)) j = (map I (component R ι M j)) ((mk I (⨁ (j : ι), M j)) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Module/Defs.lean
theorem neg_one_smul (x : M) : (-1 : R) • x = -x

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ -1 • x = -x

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma BddAbove.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ}
    (hf : BddAbove (range f)) (hg : Monotone g) : BddAbove (range (fun x => g (f x)))

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range fun x => g (f x))

Tactic:
change BddAbove (range (g ∘ f))

Result:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range (g ∘ f))

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range (g ∘ f))

Tactic:
simpa only [Set.range_comp] using hg.map_bddAbove hf

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem tendsto_nhdsWithin_nhdsWithin {t : Set β} {a b} :
    Tendsto f (𝓝[s] a) (𝓝[t] b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε :=
  (nhdsWithin_basis_eball.tendsto_iff nhdsWithin_basis_eball).trans <|
    forall₂_congr fun ε _ => exists_congr fun δ => and_congr_right fun _ =>
      forall_congr' fun x => by simp; tauto

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ x ∈ ball a δ ∩ s → f x ∈ ball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
simp

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
tauto

Result:
no goals
-- Mathlib/Topology/Order/LocalExtr.lean
/-- If `f` is antitone to the left and monotone to the right, then it has a local minimum. -/
lemma isLocalMin_of_anti_mono' {α : Type*} [TopologicalSpace α] [LinearOrder α]
    {β : Type*} [Preorder β] {b : α} {f : α → β}
    {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b)
    (h₀ : AntitoneOn f a) (h₁ : MonotoneOn f c) : IsLocalMin f b :=
  have : b ∈ a := mem_of_mem_nhdsWithin (by simp) ha
  have : b ∈ c := mem_of_mem_nhdsWithin (by simp) hc
  mem_of_superset (nhds_of_Ici_Iic ha hc) (fun x _ => by rcases le_total x b <;> aesop)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this : b ∈ a
⊢ b ∈ Ici b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
⊢ x ∈ {x | (fun x => f b ≤ f x) x}

Tactic:
rcases le_total x b <;> aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
⊢ b ∈ Iic b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Operations.lean
theorem ofReal_prod_of_nonneg {α : Type*} {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :
    ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

Proof state:
α : Type u_2
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∏ i ∈ s, f i).toNNReal = ∏ a ∈ s, (f a).toNNReal

Tactic:
exact Real.toNNReal_prod_of_nonneg hf

Result:
no goals

Proof state:
α : Type u_2
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

Tactic:
simp_rw [ENNReal.ofReal, ← coe_finset_prod, coe_inj]

Result:
α : Type u_2
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∏ i ∈ s, f i).toNNReal = ∏ a ∈ s, (f a).toNNReal
-- Mathlib/Data/Rel.lean
theorem core_univ : r.core Set.univ = Set.univ :=
  Set.ext (by simp [mem_core])

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ ∀ (x : α), x ∈ r.core Set.univ ↔ x ∈ Set.univ

Tactic:
simp [mem_core]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearMap.lean
theorem compl₁₂_id_id (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) : f.compl₁₂ LinearMap.id LinearMap.id = f

Proof state:
case h.h
R : Type u_1
inst✝⁶ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module R Mₗ
inst✝¹ : Module R Nₗ
inst✝ : Module R Pₗ
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x✝¹ : Mₗ
x✝ : Nₗ
⊢ ((f.compl₁₂ id id) x✝¹) x✝ = (f x✝¹) x✝

Tactic:
simp_rw [compl₁₂_apply, id_coe, _root_.id]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module R Mₗ
inst✝¹ : Module R Nₗ
inst✝ : Module R Pₗ
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
⊢ f.compl₁₂ id id = f

Tactic:
ext

Result:
case h.h
R : Type u_1
inst✝⁶ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module R Mₗ
inst✝¹ : Module R Nₗ
inst✝ : Module R Pₗ
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x✝¹ : Mₗ
x✝ : Nₗ
⊢ ((f.compl₁₂ id id) x✝¹) x✝ = (f x✝¹) x✝
-- Mathlib/Probability/Variance.lean
theorem evariance_zero : evariance 0 μ = 0

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ eVar[0; μ] = 0

Tactic:
simp [evariance]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem Matrix.toMatrix₂Aux_toLinearMap₂'Aux (f : Matrix n m N₂) :
    LinearMap.toMatrix₂Aux R (fun i => Pi.single i 1)
        (fun j => Pi.single j 1) (f.toLinearMap₂'Aux σ₁ σ₂) =
      f

Proof state:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
⊢ (toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) = f

Tactic:
ext i j

Result:
case a
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ (toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) i j = f i j

Proof state:
case a
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ (toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) i j = f i j

Tactic:
simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_single]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max (x y : K) :
    adicAbv v (x + y) ≤ (adicAbv v x) ⊔ (adicAbv v y)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x y : K
⊢ (adicAbv v) (x + y) ≤ (adicAbv v) x ⊔ (adicAbv v) y

Tactic:
simp [← FinitePlace.norm_def]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivative_inv' {R} [Field R] (f : R⟦X⟧) : d⁄dX R f⁻¹ = -f⁻¹ ^ 2 * d⁄dX R f

Proof state:
case pos
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : (constantCoeff R) f = 0
⊢ f⁻¹ = 0

Tactic:
rwa [MvPowerSeries.inv_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
⊢ (d⁄dX R) f⁻¹ = -f⁻¹ ^ 2 * (d⁄dX R) f

Tactic:
by_cases h : constantCoeff R f = 0

Result:
case pos
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : (constantCoeff R) f = 0
⊢ (d⁄dX R) f⁻¹ = -f⁻¹ ^ 2 * (d⁄dX R) f

case neg
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : ¬(constantCoeff R) f = 0
⊢ (d⁄dX R) f⁻¹ = -f⁻¹ ^ 2 * (d⁄dX R) f

Proof state:
case neg.h
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : ¬(constantCoeff R) f = 0
⊢ f⁻¹ * f = 1

Tactic:
exact PowerSeries.inv_mul_cancel (h := h)

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : ¬(constantCoeff R) f = 0
⊢ (d⁄dX R) f⁻¹ = -f⁻¹ ^ 2 * (d⁄dX R) f

Tactic:
apply Derivation.leibniz_of_mul_eq_one

Result:
case neg.h
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : ¬(constantCoeff R) f = 0
⊢ f⁻¹ * f = 1

Proof state:
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : (constantCoeff R) f = 0
this : f⁻¹ = 0
⊢ (d⁄dX R) f⁻¹ = -f⁻¹ ^ 2 * (d⁄dX R) f

Tactic:
rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : (constantCoeff R) f = 0
⊢ (d⁄dX R) f⁻¹ = -f⁻¹ ^ 2 * (d⁄dX R) f

Tactic:
suffices f⁻¹ = 0 by
  rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]

Result:
case pos
R : Type u_1
inst✝ : Field R
f : R⟦X⟧
h : (constantCoeff R) f = 0
⊢ f⁻¹ = 0
-- Mathlib/Topology/Sheaves/Presheaf.lean
theorem pushforward_eq' {X Y : TopCat.{w}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.Presheaf C) :
    f _* ℱ = g _* ℱ

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
⊢ (pushforward C f).obj ℱ = (pushforward C g).obj ℱ

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem exists_le_of_prod_le' (hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i) :
    ∃ i ∈ s, f i ≤ g i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s : Finset ι
hs : s.Nonempty
Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
contrapose! Hle with Hlt

Result:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s : Finset ι
hs : s.Nonempty
Hlt : ∀ i ∈ s, g i < f i
⊢ ∏ i ∈ s, g i < ∏ i ∈ s, f i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s : Finset ι
hs : s.Nonempty
Hlt : ∀ i ∈ s, g i < f i
⊢ ∏ i ∈ s, g i < ∏ i ∈ s, f i

Tactic:
exact prod_lt_prod_of_nonempty' hs Hlt

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem IsBaseChange.lift_eq (g : M →ₗ[R] Q) (x : M) : h.lift g (f x) = g x

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ (h.lift g) (f x) = g x

Tactic:
convert hF 1 x <;> rw [one_smul]

Result:
no goals

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
⊢ (h.lift g) (f x) = g x

Tactic:
have hF : ∀ (s : S) (m : M), h.lift g (s • f m) = s • g m := h.lift_eq _

Result:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ (h.lift g) (f x) = g x
-- Mathlib/Data/Nat/Size.lean
theorem size_one : size 1 = 1 :=
  show size (bit true 0) = 1 by rw [size_bit, size_zero]; exact Nat.one_ne_zero

Proof state:
⊢ bit true 0 ≠ 0

Tactic:
exact Nat.one_ne_zero

Result:
no goals

Proof state:
⊢ (bit true 0).size = 1

Tactic:
rw [size_bit, size_zero]

Result:
⊢ bit true 0 ≠ 0
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_eq_restrict_iUnion_iff [Countable ι] (s : ι → Set α) (f g : α → δ) :
    f =ᵐ[μ.restrict (⋃ i, s i)] g ↔ ∀ i, f =ᵐ[μ.restrict (s i)] g

Proof state:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ f =ᶠ[ae (μ.restrict (⋃ i, s i))] g ↔ ∀ (i : ι), f =ᶠ[ae (μ.restrict (s i))] g

Tactic:
simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem singleton_eq_iff_domain (f g : Y ⟶ X) : singleton f g ↔ f = g

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ singleton f f

Tactic:
apply singleton.mk

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g → f = g

Tactic:
rintro ⟨a, rfl⟩

Result:
case mp.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ f = f

Proof state:
case mp.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ f = f

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g

Tactic:
rintro rfl

Result:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ singleton f f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g ↔ f = g

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g → f = g

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem exists_deriv_eq_slope' : ∃ c ∈ Ioo a b, deriv f c = slope f a b

Proof state:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, deriv f c = slope f a b

Tactic:
rw [slope_def_field]

Result:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a)

Proof state:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a)

Tactic:
exact exists_deriv_eq_slope f hab hfc hfd

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial.lean
theorem quotient_mk_comp_C_injective [Field K] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) :
    Function.Injective ((Ideal.Quotient.mk I).comp MvPolynomial.C)

Proof state:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ((Ideal.Quotient.mk I).comp C) x = 0
⊢ x = 0

Tactic:
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem] at hx

Result:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
⊢ x = 0

Proof state:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I

Tactic:
have := I.mul_mem_left (MvPolynomial.C x⁻¹) hx

Result:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
hx0 : ¬x = 0
this : C x⁻¹ * C x ∈ I
⊢ 1 ∈ I

Proof state:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
⊢ Function.Injective ⇑((Ideal.Quotient.mk I).comp C)

Tactic:
refine (injective_iff_map_eq_zero _).2 fun x hx => ?_

Result:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ((Ideal.Quotient.mk I).comp C) x = 0
⊢ x = 0

Proof state:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
hx0 : ¬x = 0
this : C x⁻¹ * C x ∈ I
⊢ 1 ∈ I

Tactic:
rwa [← MvPolynomial.C.map_mul, inv_mul_cancel₀ hx0, MvPolynomial.C_1] at this

Result:
no goals

Proof state:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
⊢ x = 0

Tactic:
refine _root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 ?_) hI

Result:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I
-- Mathlib/SetTheory/Cardinal/ENat.lean
theorem toENat_lift {a : Cardinal.{v}} : toENat (lift.{u} a) = toENat a

Proof state:
case inr
a : Cardinal.{v}
ha : ℵ₀ ≤ a
⊢ toENat (lift.{u, v} a) = toENat a

Tactic:
simp [toENat_eq_top.2, ha]

Result:
no goals

Proof state:
case inl.intro
a : ℕ∞
⊢ toENat (lift.{u, v} ↑a) = toENat ↑a

Tactic:
simp

Result:
no goals

Proof state:
case inl
a : Cardinal.{v}
ha : a ≤ ℵ₀
⊢ toENat (lift.{u, v} a) = toENat a

Tactic:
lift a to ℕ∞ using ha

Result:
case inl.intro
a : ℕ∞
⊢ toENat (lift.{u, v} ↑a) = toENat ↑a

Proof state:
a : Cardinal.{v}
⊢ toENat (lift.{u, v} a) = toENat a

Tactic:
cases le_total a ℵ₀ with
| inl ha => lift a to ℕ∞ using ha; simp
| inr ha => simp [toENat_eq_top.2, ha]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
private lemma exists_lt_add_left {a b c : EReal} (hc : c < a + b) : ∃ a' < a, c < a' + b

Proof state:
case intro.intro
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ b ≠ ⊥

Tactic:
contrapose! hc

Result:
case intro.intro
a b c a' : EReal
hc' : c - b < a'
ha' : a' < a
hc : b = ⊥
⊢ a + b ≤ c

Proof state:
case intro.intro
a b c a' : EReal
hc' : c - b < a'
ha' : a' < a
hc : b = ⊥
⊢ a + b ≤ c

Tactic:
exact hc ▸ (add_bot a).symm ▸ bot_le

Result:
no goals

Proof state:
a b c : EReal
hc : c < a + b
⊢ ∃ a' < a, c < a' + b

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (sub_lt_of_lt_add hc)

Result:
case intro.intro
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' + b

Proof state:
case intro.intro
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' + b

Tactic:
refine ⟨a', ha', (sub_lt_iff (.inl ?_) (.inr hc.ne_top)).1 hc'⟩

Result:
case intro.intro
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ b ≠ ⊥
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem IsMaximal.of_isMaximal_liesOver [P.IsMaximal] : p.IsMaximal

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsMaximal
⊢ (Ideal.under A P).IsMaximal

Tactic:
exact isMaximal_comap_of_isIntegral_of_isMaximal P

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsMaximal
⊢ p.IsMaximal

Tactic:
rw [P.over_def p]

Result:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsMaximal
⊢ (Ideal.under A P).IsMaximal
-- Mathlib/Data/Fintype/Inv.lean
theorem invFun_restrict [Nonempty α] : (Set.range f).restrict (invFun f) = hf.invOfMemRange

Proof state:
case h.mk.a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ f ((Set.range f).restrict (invFun f) ⟨b, h⟩) = f (hf.invOfMemRange ⟨b, h⟩)

Tactic:
simp [hf.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]

Result:
no goals

Proof state:
case h.mk
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ (Set.range f).restrict (invFun f) ⟨b, h⟩ = hf.invOfMemRange ⟨b, h⟩

Tactic:
apply hf

Result:
case h.mk.a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ f ((Set.range f).restrict (invFun f) ⟨b, h⟩) = f (hf.invOfMemRange ⟨b, h⟩)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
⊢ (Set.range f).restrict (invFun f) = hf.invOfMemRange

Tactic:
ext ⟨b, h⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ (Set.range f).restrict (invFun f) ⟨b, h⟩ = hf.invOfMemRange ⟨b, h⟩
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp]
lemma expect_neg_distrib (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
⊢ 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i

Tactic:
simp [expect]

Result:
no goals