harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway {Rᵣ : Type*} [CommRing Rᵣ]
    [Algebra R Rᵣ] (r : R) [IsLocalization.Away r Rᵣ] :
    IsStandardSmoothOfRelativeDimension.{0, 0} 0 (algebraMap R Rᵣ)

Proof state:
case h
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (let_fun I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
rw [Algebra.smul_def]

Result:
case h
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (let_fun I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    (algebraMap R Rᵣ) r✝ * x✝

Proof state:
case h
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (let_fun I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    (algebraMap R Rᵣ) r✝ * x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
⊢ (algebraMap R Rᵣ).toAlgebra = inst✝¹

Tactic:
ext

Result:
case h
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (let_fun I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Proof state:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
this : (algebraMap R Rᵣ).toAlgebra = inst✝¹
⊢ Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.localization_away r

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)

Tactic:
have : (algebraMap R Rᵣ).toAlgebra = ‹Algebra R Rᵣ› := by
  ext
  rw [Algebra.smul_def]
  rfl

Result:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
this : (algebraMap R Rᵣ).toAlgebra = inst✝¹
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)

Proof state:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
this : (algebraMap R Rᵣ).toAlgebra = inst✝¹
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)

Tactic:
rw [IsStandardSmoothOfRelativeDimension, this]

Result:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
this : (algebraMap R Rᵣ).toAlgebra = inst✝¹
⊢ Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ
-- Mathlib/Computability/TuringMachine.lean
theorem step_supports (M : Λ → Stmt Γ Λ σ) {S : Finset Λ} (ss : Supports M S) :
    ∀ {c c' : Cfg Γ Λ σ}, c' ∈ step M c → c.l ∈ Finset.insertNone S → c'.l ∈ Finset.insertNone S
  | ⟨some l₁, v, T⟩, c', h₁, h₂ => by
    replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂)
    simp only [step, Option.mem_def, Option.some.injEq] at h₁; subst c'
    revert h₂; induction M l₁ generalizing v T with intro hs
    | branch p q₁' q₂' IH₁ IH₂ =>
      unfold stepAux; cases p v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1
    | goto => exact Finset.some_mem_insertNone.2 (hs _)
    | halt => apply Multiset.mem_cons_self
    | load _ _ IH | _ _ _ _ IH => exact IH _ _ hs

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₁ : c' ∈ step M { l := some l₁, var := v, stk := T }
h₂ : SupportsStmt S (M l₁)
⊢ c'.l ∈ Finset.insertNone S

Tactic:
simp only [step, Option.mem_def, Option.some.injEq] at h₁

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₂ : SupportsStmt S (M l₁)
h₁ : stepAux (M l₁) v T = c'
⊢ c'.l ∈ Finset.insertNone S
-- Mathlib/Analysis/PSeries.lean
theorem le_tsum_schlomilch (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
    (hu : StrictMono u) :
    ∑' k , f k ≤ ∑ k ∈ range (u 0), f k + ∑' k : ℕ, (u (k + 1) - u k) * f (u k)

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)
⊢ ∑ x ∈ range n, ↑(u (x + 1) - u x) * f (u x) ≤ ∑' (k : ℕ), ↑(u (k + 1) - u k) * f (u k)

Tactic:
apply ENNReal.sum_le_tsum

Result:
no goals

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Tactic:
simp only [nsmul_eq_mul, this]

Result:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)
⊢ ∑ x ∈ range n, ↑(u (x + 1) - u x) * f (u x) ≤ ∑' (k : ℕ), ↑(u (k + 1) - u k) * f (u k)

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
⊢ ⨆ i, ∑ a ∈ range (u i), f a ≤ ∑ k ∈ range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Tactic:
refine iSup_le fun n =>
  (Finset.le_sum_schlomilch hf h_pos hu.monotone n).trans (add_le_add_left ?_ _)

Result:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
⊢ ∑' (k : ℕ), f k ≤ ∑ k ∈ range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' hu.tendsto_atTop]

Result:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
⊢ ⨆ i, ∑ a ∈ range (u i), f a ≤ ∑ k ∈ range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n k : ℕ
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)

Tactic:
simp [NNReal.coe_sub (Nat.cast_le (α := ℝ≥0).mpr <| (hu k.lt_succ_self).le)]

Result:
no goals

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Tactic:
have (k : ℕ) : (u (k + 1) - u k : ℝ≥0∞) = (u (k + 1) - (u k : ℕ) : ℕ) := by
  simp [NNReal.coe_sub (Nat.cast_le (α := ℝ≥0).mpr <| (hu k.lt_succ_self).le)]

Result:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem sum_over_range' [AddCommMonoid S] (p : R[X]) {f : ℕ → R → S} (h : ∀ n, f n 0 = 0) (n : ℕ)
    (w : p.natDegree < n) : p.sum f = ∑ a ∈ range n, f a (coeff p a)

Proof state:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : { toFinsupp := toFinsupp✝ }.natDegree < n
this : toFinsupp✝.support ⊆ range n
⊢ ∑ x ∈ toFinsupp✝.support, f x (toFinsupp✝ x) = ∑ x ∈ range n, f x (toFinsupp✝ x)

Tactic:
exact Finsupp.sum_of_support_subset _ this _ fun n _hn => h n

Result:
no goals

Proof state:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : { toFinsupp := toFinsupp✝ }.natDegree < n
⊢ { toFinsupp := toFinsupp✝ }.sum f = ∑ a ∈ range n, f a ({ toFinsupp := toFinsupp✝ }.coeff a)

Tactic:
have := supp_subset_range w

Result:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : { toFinsupp := toFinsupp✝ }.natDegree < n
this : { toFinsupp := toFinsupp✝ }.support ⊆ range n
⊢ { toFinsupp := toFinsupp✝ }.sum f = ∑ a ∈ range n, f a ({ toFinsupp := toFinsupp✝ }.coeff a)

Proof state:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : { toFinsupp := toFinsupp✝ }.natDegree < n
this : { toFinsupp := toFinsupp✝ }.support ⊆ range n
⊢ { toFinsupp := toFinsupp✝ }.sum f = ∑ a ∈ range n, f a ({ toFinsupp := toFinsupp✝ }.coeff a)

Tactic:
simp only [Polynomial.sum, support, coeff, natDegree, degree] at this ⊢

Result:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : { toFinsupp := toFinsupp✝ }.natDegree < n
this : toFinsupp✝.support ⊆ range n
⊢ ∑ x ∈ toFinsupp✝.support, f x (toFinsupp✝ x) = ∑ x ∈ range n, f x (toFinsupp✝ x)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
w : p.natDegree < n
⊢ p.sum f = ∑ a ∈ range n, f a (p.coeff a)

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : { toFinsupp := toFinsupp✝ }.natDegree < n
⊢ { toFinsupp := toFinsupp✝ }.sum f = ∑ a ∈ range n, f a ({ toFinsupp := toFinsupp✝ }.coeff a)
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.isLUB_Iio (ha : IsSuccPrelimit a) : IsLUB (Iio a) a

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
⊢ IsLUB (Iio a) a

Tactic:
refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩

Result:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
⊢ c < b

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
⊢ c < b

Tactic:
obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc

Result:
case intro.intro
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
d : α
hd : d < a
hd' : c < d
⊢ c < b

Proof state:
case intro.intro
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
d : α
hd : d < a
hd' : c < d
⊢ c < b

Tactic:
exact hd'.trans_le (hb hd)

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem isSimpleModule_iff_quot_maximal :
    IsSimpleModule R M ↔ ∃ I : Ideal R, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Proof state:
case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
exact ⟨_, ker_toSpanSingleton_isMaximal R hm,
  ⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩

Result:
no goals

Proof state:
case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
this : Nontrivial M
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
have ⟨m, hm⟩ := exists_ne (0 : M)

Result:
case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Proof state:
case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
have := IsSimpleModule.nontrivial R M

Result:
case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
this : Nontrivial M
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Proof state:
case refine_2
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R (R ⧸ I)

Tactic:
rwa [isSimpleModule_iff_isCoatom]

Result:
no goals

Proof state:
case refine_2
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R M

Tactic:
convert congr equiv

Result:
case refine_2
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R (R ⧸ I)

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleModule R M ↔ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩

Result:
case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

case refine_2
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R M
-- Mathlib/Probability/Variance.lean
lemma evariance_eq_top_iff [IsFiniteMeasure μ] (hX : AEStronglyMeasurable X μ) :
    evariance X μ = ∞ ↔ ¬ MemLp X 2 μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] = ⊤ ↔ ¬MemLp X 2 μ

Tactic:
simp [← evariance_lt_top_iff_memLp hX]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem Ideal.IsPrincipal.of_comap (f : F) (hf : Function.Surjective f) (I : Ideal S)
    [hI : IsPrincipal (I.comap f)] : IsPrincipal I

Proof state:
R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal I

Tactic:
rw [← map_comap_of_surjective f hf I]

Result:
R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal (map f (comap f I))

Proof state:
R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal (map f (comap f I))

Tactic:
exact hI.map_ringHom f

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem reduce.red : Red L (reduce L)

Proof state:
case pos.mk.mk
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
h : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = !(fst✝, snd✝).2
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2

Tactic:
cases h

Result:
case pos.mk.mk.intro
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
right✝ : (fst✝¹, snd✝¹).2 = !(fst✝, snd✝).2
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2

Proof state:
case nil
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])

Tactic:
constructor

Result:
no goals

Proof state:
case neg
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)

Tactic:
exact Red.cons_cons ih

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1] (fun head tail tail_ih => if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
      [])

Tactic:
exact Red.cons_cons ih

Result:
no goals
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageSubobjectIso_imageToKernel' (w : f ≫ g = 0) :
    (imageSubobjectIso f).hom ≫ imageToKernel' f g w =
      imageToKernel f g w ≫ (kernelSubobjectIso g).hom

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0

Tactic:
simp [imageToKernel']

Result:
no goals

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (kernelSubobjectIso g).hom

Tactic:
ext

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem zmod_char_ne_one_iff (n : ℕ) [NeZero n] (ψ : AddChar (ZMod n) C) : ψ ≠ 1 ↔ ψ 1 ≠ 1

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
⊢ ψ a = 1

Tactic:
have ha₁ : a = a.val • (1 : ZMod ↑n) := by
  rw [nsmul_eq_mul, mul_one]; exact (ZMod.natCast_zmod_val a).symm

Result:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
ha₁ : a = a.val • 1
⊢ ψ a = 1

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ ψ ≠ 1 ↔ ψ 1 ≠ 1

Tactic:
rw [ne_one_iff]

Result:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ (∃ x, ψ x ≠ 1) ↔ ψ 1 ≠ 1

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ (∃ x, ψ x ≠ 1) → ψ 1 ≠ 1

Tactic:
contrapose!

Result:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ ψ 1 = 1 → ∀ (x : ZMod n), ψ x = 1

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
⊢ a = ↑a.val

Tactic:
exact (ZMod.natCast_zmod_val a).symm

Result:
no goals

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
⊢ a = a.val • 1

Tactic:
rw [nsmul_eq_mul, mul_one]

Result:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
⊢ a = ↑a.val

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ ψ 1 = 1 → ∀ (x : ZMod n), ψ x = 1

Tactic:
rintro h₁ a

Result:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
⊢ ψ a = 1

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
ha₁ : a = a.val • 1
⊢ ψ a = 1

Tactic:
rw [ha₁, map_nsmul_eq_pow, h₁, one_pow]

Result:
no goals

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ (∃ x, ψ x ≠ 1) ↔ ψ 1 ≠ 1

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

Result:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ (∃ x, ψ x ≠ 1) → ψ 1 ≠ 1
-- Mathlib/CategoryTheory/Sites/OneHypercover.lean
@[reassoc]
lemma multiforkLift_map (i₀ : E.I₀) : multiforkLift c ≫ F.val.map (E.f i₀).op = c.ι i₀

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{u_3, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.val)
i₀ : E.I₀
⊢ multiforkLift c ≫ F.val.map (E.f i₀).op = c.ι i₀

Tactic:
simp [multiforkLift]

Result:
no goals
-- Mathlib/Data/W/Constructions.lean
theorem rightInverse_nat : Function.RightInverse ofNat toNat
  | Nat.zero => rfl
  | Nat.succ n => by rw [ofNat, toNat, rightInverse_nat n]

Proof state:
n : ℕ
⊢ (ofNat n.succ).toNat = n.succ

Tactic:
rw [ofNat, toNat, rightInverse_nat n]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma min_assoc (a b c : α) : min (min a b) c = min a (min b c)

Proof state:
case h₃.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ c

Tactic:
apply le_trans h₂

Result:
case h₃.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ min b c ≤ c

Proof state:
case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ min (min a b) c

Tactic:
apply le_min

Result:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ min a b

case h₃.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ c

Proof state:
case h₂.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ b

Tactic:
apply le_trans (min_le_left ..) (min_le_right ..)

Result:
no goals

Proof state:
case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) c

Tactic:
intro d h₁ h₂

Result:
case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ min (min a b) c

Proof state:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ min a b

Tactic:
apply le_min h₁

Result:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ b

Proof state:
case h₃.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ min b c ≤ c

Tactic:
apply min_le_right

Result:
no goals

Proof state:
case h₂.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ c

Tactic:
apply min_le_right

Result:
no goals

Proof state:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ b

Tactic:
apply le_trans h₂

Result:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ min b c ≤ b

Proof state:
case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ min b c

Tactic:
apply le_min

Result:
case h₂.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ b

case h₂.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ c

Proof state:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ min b c ≤ b

Tactic:
apply min_le_left

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ a

Tactic:
apply le_trans (min_le_left ..) (min_le_left ..)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c = min a (min b c)

Tactic:
apply eq_min

Result:
case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ a

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ min b c

case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) c