harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Seq/Seq.lean
theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂

Proof state:
case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
have this := congr_arg destruct e

Result:
case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Proof state:
case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ nil.append s₂ → nil.append s₂ = cons b s' → a ∈ nil ∨ a ∈ s₂

Tactic:
intro m _

Result:
case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ nil ∨ a ∈ s₂

Proof state:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ (b : α) (s' : Seq α),
    (a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) →
      ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂

Tactic:
intro b s' o s₁

Result:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
⊢ a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = ss → a ∈ s₁ ∨ a ∈ s₂

Tactic:
apply mem_rec_on h _

Result:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ (b : α) (s' : Seq α),
    (a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) →
      ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
⊢ a = c ∨ a ∈ t₁.append s₂

Tactic:
simpa using m

Result:
no goals

Proof state:
case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂

Tactic:
exact Or.inl (mem_cons _ _)

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_hnot_sdiff_distrib (a b : α) : ￢￢(a \ b) = ￢￢a \ ￢￢b

Proof state:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)

Tactic:
rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm, ←
  hnot_le_iff_codisjoint_right]

Result:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b

Proof state:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢a \ ￢￢b ≤ ￢￢(a \ b)

Tactic:
rw [sdiff_le_iff, ← hnot_hnot_sup_distrib]

Result:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢(b ⊔ a \ b)

Proof state:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢(b ⊔ a \ b)

Tactic:
exact hnot_anti (hnot_anti le_sup_sdiff)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢(a \ b) = ￢￢a \ ￢￢b

Tactic:
apply le_antisymm

Result:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b

case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢a \ ￢￢b ≤ ￢￢(a \ b)

Proof state:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b

Tactic:
exact le_sdiff_sup

Result:
no goals

Proof state:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b

Tactic:
refine hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' ?_)

Result:
case a
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
     (#[a] ++ xs).lex (#[b] ++ ys) lt =
       (lt a b || a == b && xs.lex ys lt)

Proof state:
case true
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (match
      (match
          if true = true then ForInStep.done ⟨some true, PUnit.unit⟩
          else
            if (a != b) = true then ForInStep.done ⟨some false, PUnit.unit⟩ else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b_1 =>
          forIn' (List.range' 0 (min xs.size ys.size) 1) b_1 fun a_1 m b_2 =>
            if lt xs[a_1] ys[a_1] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (xs[a_1] != ys[a_1]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => decide (xs.size < ys.size)
    | some a => a) =
    (true ||
      a == b &&
        match
          (forIn' (List.range' 0 (min xs.size ys.size) 1) ⟨none, PUnit.unit⟩ fun a m b =>
              if lt xs[a] ys[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
              else
                if (xs[a] != ys[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
                else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
        | none => decide (xs.size < ys.size)
        | some a => a)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem mul {x y : K_hat R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) :
    (x * y).IsFiniteAdele

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : Valued.v (x v) ≤ 1 ∧ Valued.v (y v) ≤ 1
h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v)
⊢ Valued.v (x v) * Valued.v (y v) ≤ 1

Tactic:
exact mul_le_one' hv.left hv.right

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : (x * y) v ∉ adicCompletionIntegers K v
⊢ x v ∉ adicCompletionIntegers K v ∨ y v ∉ adicCompletionIntegers K v

Tactic:
contrapose! hv

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x * y) v ∈ adicCompletionIntegers K v

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K_hat R K
hx : x.IsFiniteAdele
hy : y.IsFiniteAdele
⊢ (x * y).IsFiniteAdele

Tactic:
rw [IsFiniteAdele, Filter.eventually_cofinite] at hx hy ⊢

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
⊢ {x_1 | (x * y) x_1 ∉ adicCompletionIntegers K x_1}.Finite
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem exists_spanning_measurableSet_le {f : α → ℝ≥0} (hf : Measurable f) (μ : Measure α)
    [SigmaFinite μ] :
    ∃ s : ℕ → Set α,
      (∀ n, MeasurableSet (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, f x ≤ n) ∧
      ⋃ i, s i = Set.univ

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n => {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
⊢ f x ≤ ↑i → f x ≤ ↑j

Tactic:
refine fun hif => hif.trans ?_

Result:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n => {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
hif : f x ≤ ↑i
⊢ ↑i ≤ ↑j
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
/-- See `MemLp.prod'` for the applied version. -/
protected lemma MemLp.prod (hf : ∀ i ∈ s, MemLp (f i) (p i) μ) :
    MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Proof state:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) (p i) μ) → MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ (p i)⁻¹ + (∑ i ∈ s, (p i)⁻¹)⁻¹⁻¹ = (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case cons
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) (p i) μ) → MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp (∏ i ∈ cons i s hi, f i) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ

Tactic:
rw [prod_cons]

Result:
case cons
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) (p i) μ) → MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp (f i * ∏ x ∈ s, f x) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ

Proof state:
case cons
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) (p i) μ) → MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp (f i * ∏ x ∈ s, f x) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ

Tactic:
exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

Result:
no goals

Proof state:
case empty
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ ∅, MemLp (f i) (p i) μ
⊢ MemLp (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

Tactic:
by_cases hμ : μ = 0 <;>
  simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
⊢ MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Tactic:
induction s using cons_induction with
| empty =>
  by_cases hμ : μ = 0 <;>
    simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]
| cons i s hi ih =>
  rw [prod_cons]
  exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
    a ^ n < a ^ m ↔ n < m

Proof state:
case mpr
a n m : Nat
h : 1 < a
⊢ n < m → a ^ n < a ^ m

Tactic:
intro w

Result:
case mpr
a n m : Nat
h : 1 < a
w : n < m
⊢ a ^ n < a ^ m

Proof state:
case mpr
a n m : Nat
h : 1 < a
w : n < m
⊢ a ^ n < a ^ m

Tactic:
exact Nat.pow_lt_pow_of_lt h w

Result:
no goals

Proof state:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n < a ^ m ∧ m ≤ n
⊢ False

Tactic:
apply Nat.lt_irrefl (a ^ n)

Result:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n < a ^ m ∧ m ≤ n
⊢ a ^ n < a ^ n

Proof state:
case mp.a
a n m : Nat
h : 1 < a
w : ¬(a ^ n < a ^ m → n < m)
⊢ False

Tactic:
simp at w

Result:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n < a ^ m ∧ m ≤ n
⊢ False

Proof state:
case mp
a n m : Nat
h : 1 < a
⊢ a ^ n < a ^ m → n < m

Tactic:
apply Decidable.by_contra

Result:
case mp.a
a n m : Nat
h : 1 < a
⊢ ¬(a ^ n < a ^ m → n < m) → False

Proof state:
a n m : Nat
h : 1 < a
⊢ a ^ n < a ^ m ↔ n < m

Tactic:
constructor

Result:
case mp
a n m : Nat
h : 1 < a
⊢ a ^ n < a ^ m → n < m

case mpr
a n m : Nat
h : 1 < a
⊢ n < m → a ^ n < a ^ m

Proof state:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n < a ^ m ∧ m ≤ n
⊢ a ^ n < a ^ n

Tactic:
exact Nat.lt_of_lt_of_le w.1 (Nat.pow_le_pow_of_le h w.2)

Result:
no goals

Proof state:
case mp.a
a n m : Nat
h : 1 < a
⊢ ¬(a ^ n < a ^ m → n < m) → False

Tactic:
intros w

Result:
case mp.a
a n m : Nat
h : 1 < a
w : ¬(a ^ n < a ^ m → n < m)
⊢ False
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_mul_zeta : Λ * ζ = log

Proof state:
case h
n : ℕ
⊢ Real.log ↑n = log n

Tactic:
rfl

Result:
no goals

Proof state:
case h
n : ℕ
⊢ (Λ * ↑ζ) n = log n

Tactic:
rw [coe_mul_zeta_apply, vonMangoldt_sum]

Result:
case h
n : ℕ
⊢ Real.log ↑n = log n

Proof state:
⊢ Λ * ↑ζ = log

Tactic:
ext n

Result:
case h
n : ℕ
⊢ (Λ * ↑ζ) n = log n
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_pf_add_overlap_zero
    (h : IsNat (a₁ + b₁) (nat_lit 0)) (h₄ : a₂ + b₂ = c) : (a₁ + a₂ : R) + (b₁ + b₂) = c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂

Tactic:
rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma IsGreatest.nnnorm_cfcₙ_nnreal (f : ℝ≥0 → ℝ≥0) (a : A)
    (hf : ContinuousOn f (σₙ ℝ≥0 a)

Proof state:
case h.e'_3.h
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
⊢ x ∈ f '' σₙ ℝ≥0 a ↔ x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

Tactic:
constructor

Result:
case h.e'_3.h.mp
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
⊢ x ∈ f '' σₙ ℝ≥0 a → x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

case h.e'_3.h.mpr
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
⊢ x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a → x ∈ f '' σₙ ℝ≥0 a

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (σₙ ℝ a)

Tactic:
exact continuous_subtype_val.comp_continuousOn <|
ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

Result:
no goals
-- Mathlib/RepresentationTheory/Character.lean
theorem char_one (V : FDRep k G) : V.character 1 = Module.finrank k V

Proof state:
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V : FDRep k G
⊢ V.character 1 = ↑(finrank k ↑V.V)

Tactic:
simp only [character, map_one, trace_one]

Result:
no goals
-- Mathlib/Topology/Category/CompHaus/Basic.lean
theorem epi_iff_surjective {X Y : CompHaus.{u}} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f

Proof state:
case intro
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X => ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
y' : (fun X => ↑X.toTop) X
hy' : (ConcreteCategory.hom f) y' = y
⊢ False

Tactic:
exact hy y' hy'

Result:
no goals

Proof state:
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
constructor

Result:
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Proof state:
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X => ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X => ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X => ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x => True) { toFun := fun y' => { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x => True) { toFun := fun x => { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
H : 0 = 1
⊢ False

Tactic:
exact zero_ne_one H

Result:
no goals

Proof state:
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
rw [← CategoryTheory.epi_iff_surjective]

Result:
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Epi ⇑(ConcreteCategory.hom f) → Epi f

Proof state:
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X => ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ False

Tactic:
have hCD : Disjoint C D := by
  rw [Set.disjoint_singleton_right]
  rintro ⟨y', hy'⟩
  exact hy y' hy'

Result:
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X => ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
⊢ False
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma det_det_aux
    (ih : ∀ M, (f (det M)).det = ((M.map f).comp {a // (a = k) = False} _ n n R).det) :
    ((f M.det).det - ((M.map f).comp m m n n R).det) *
      (f (M k k)).det ^ (Fintype.card m - 1) = 0

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ ((f M.det).det - ((Matrix.comp m m n n R) (M.map ⇑f)).det) * (f (M k k)).det ^ (Fintype.card m - 1) = 0

Tactic:
rw [sub_mul, comp_det_mul_pow, ← det_pow, ← map_pow, ← det_mul, ← _root_.map_mul,
  det_mul_corner_pow, _root_.map_mul, det_mul, ih, sub_self]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem posDef_pi_iff {P} [Fintype ι] [OrderedAddCommMonoid P] [Module R P]
    {Q : ∀ i, QuadraticMap R (Mᵢ i) P} : (pi Q).PosDef ↔ ∀ i, (Q i).PosDef

Proof state:
case mp.intro
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
hle : ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
ha : (pi Q).Anisotropic
i : ι
⊢ (∀ (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (Q i).Anisotropic

Tactic:
exact ⟨hle i, anisotropic_of_pi ha i⟩

Result:
no goals