harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TuringMachine.lean
theorem tr_respects : Respects (TM2.step M) (TM1.step (tr M)) TrCfg

Proof state:
case H₃
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₁ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₂ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L))) b
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ ∃ b,
    TrCfg (bif p v then TM2.stepAux q₁ v S else TM2.stepAux q₂ v S) b ∧
      Reaches (TM1.step (tr M))
        (bif (fun x => p) (Tape.mk' ∅ (addBottom L)).head v then TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))
        else TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L)))
        b

Tactic:
beta_reduce

Result:
case H₃
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₁ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₂ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L))) b
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ ∃ b,
    TrCfg (bif p v then TM2.stepAux q₁ v S else TM2.stepAux q₂ v S) b ∧
      Reaches (TM1.step (tr M))
        (bif p v then TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))
        else TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L)))
        b
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem sound (U : Set (G ⧸ N)) (g : N.op) :
    g • (mk' N) ⁻¹' U = (mk' N) ⁻¹' U

Proof state:
case h.a.h.e'_5
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ (mk' N) (g⁻¹ • x) = (mk' N) x

Tactic:
exact Quotient.sound ⟨g⁻¹, rfl⟩

Result:
no goals

Proof state:
case h
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ (mk' N) (g⁻¹ • x) ∈ U ↔ (mk' N) x ∈ U

Tactic:
congr! 1

Result:
case h.a.h.e'_5
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ (mk' N) (g⁻¹ • x) = (mk' N) x

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
⊢ g • ⇑(mk' N) ⁻¹' U = ⇑(mk' N) ⁻¹' U

Tactic:
ext x

Result:
case h
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ x ∈ g • ⇑(mk' N) ⁻¹' U ↔ x ∈ ⇑(mk' N) ⁻¹' U

Proof state:
case h
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ x ∈ g • ⇑(mk' N) ⁻¹' U ↔ x ∈ ⇑(mk' N) ⁻¹' U

Tactic:
simp only [Set.mem_preimage, Set.mem_smul_set_iff_inv_smul_mem]

Result:
case h
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ (mk' N) (g⁻¹ • x) ∈ U ↔ (mk' N) x ∈ U
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_antitoneOn_Icc_left (hb : b < 0) :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Icc a b)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ AntitoneOn (fun x => x⁻¹) (Set.Icc a b)

Tactic:
convert sub_inv_antitoneOn_Icc_left hb

Result:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
x✝ : α
⊢ x✝ = x✝ - 0

Proof state:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
x✝ : α
⊢ x✝ = x✝ - 0

Tactic:
exact (sub_zero _).symm

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
@[simp]
lemma bnot_comp_isNone : (! ·) ∘ @Option.isNone α = Option.isSome

Proof state:
case h
α : Type u_1
x : Option α
⊢ ((fun x => !x) ∘ isNone) x = x.isSome

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ (fun x => !x) ∘ isNone = isSome

Tactic:
funext x

Result:
case h
α : Type u_1
x : Option α
⊢ ((fun x => !x) ∘ isNone) x = x.isSome
-- Mathlib/Algebra/Group/AddChar.lean
lemma sum_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
    (∑ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a

Proof state:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ (∑ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

Tactic:
rw [coe_sum, Finset.prod_apply]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIci : Fintype.card (Set.Ici a) = n - a

Proof state:
n : ℕ
a : Fin n
⊢ Fintype.card ↑(Set.Ici a) = n - ↑a

Tactic:
rw [Fintype.card_ofFinset, card_Ici]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_replace (l : List α) (a b : α) (w) :
    (l.replace a b).head w =
      if a == l.head (by rintro rfl; simp_all) then
        b
      else
        l.head  (by rintro rfl; simp_all)

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a b : α
w : l.replace a b ≠ []
⊢ (l.replace a b).head w = if (a == l.head ⋯) = true then b else l.head ⋯

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
inst✝ : BEq α
l : List α
a b : α
w : l.replace a b ≠ []
⊢ some ((l.replace a b).head w) = some (if (a == l.head ⋯) = true then b else l.head ⋯)

Proof state:
α : Type ?u.369492
inst✝ : BEq α
a b : α
w : [].replace a b ≠ []
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case x
α : Type u_1
inst✝ : BEq α
l : List α
a b : α
w : l.replace a b ≠ []
⊢ some ((l.replace a b).head w) = some (if (a == l.head ⋯) = true then b else l.head ⋯)

Tactic:
rw [← head?_eq_head, head?_replace, head?_eq_head]

Result:
no goals

Proof state:
α : Type ?u.369492
inst✝ : BEq α
l : List α
a b : α
w : l.replace a b ≠ []
⊢ l ≠ []

Tactic:
rintro rfl

Result:
α : Type ?u.369492
inst✝ : BEq α
a b : α
w : [].replace a b ≠ []
⊢ False
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_one : ((1 : R[X]) : PowerSeries R) = 1

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ ↑1 = 1

Tactic:
have := coe_monomial 0 (1 : R)

Result:
R : Type u_1
inst✝ : CommSemiring R
this : ↑((monomial 0) 1) = (PowerSeries.monomial R 0) 1
⊢ ↑1 = 1

Proof state:
R : Type u_1
inst✝ : CommSemiring R
this : ↑((monomial 0) 1) = (PowerSeries.monomial R 0) 1
⊢ ↑1 = 1

Tactic:
rwa [PowerSeries.monomial_zero_eq_C_apply] at this

Result:
no goals
-- Mathlib/NumberTheory/SiegelsLemma.lean
private lemma card_S_eq [DecidableEq α] : #(Finset.Icc N P) = ∏ i : α, (P i - N i + 1)

Proof state:
case e_f
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ (fun i => ↑(#(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺)))) = fun i => P i - N i + 1

Tactic:
ext i

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ ↑(#(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺))) = P i - N i + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ∏ i : α, ↑(#(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺))) = ∏ i : α, (P i - N i + 1)

Tactic:
congr

Result:
case e_f
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ (fun i => ↑(#(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺)))) = fun i => P i - N i + 1

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ P i + 1 - N i = P i - N i + 1

Tactic:
exact add_sub_right_comm (P i) 1 (N i)

Result:
no goals

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ ↑(#(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺))) = P i - N i + 1

Tactic:
rw [Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)]

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ P i + 1 - N i = P i - N i + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ↑(#S) = ∏ i : α, (P i - N i + 1)

Tactic:
rw [Pi.card_Icc N P, Nat.cast_prod]

Result:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ∏ i : α, ↑(#(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺))) = ∏ i : α, (P i - N i + 1)
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem comp_eval₂Hom [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) :
    φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i => φ (g i)

Proof state:
case hX
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ ∀ (i : σ), (φ.comp (eval₂Hom f g)) (X i) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (X i)

Tactic:
intro i

Result:
case hX
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
i : σ
⊢ (φ.comp (eval₂Hom f g)) (X i) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (X i)

Proof state:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ ∀ (r : R), (φ.comp (eval₂Hom f g)) (C r) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (C r)

Tactic:
intro r

Result:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
r : R
⊢ (φ.comp (eval₂Hom f g)) (C r) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (C r)

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i => φ (g i)

Tactic:
apply MvPolynomial.ringHom_ext

Result:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ ∀ (r : R), (φ.comp (eval₂Hom f g)) (C r) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (C r)

case hX
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ ∀ (i : σ), (φ.comp (eval₂Hom f g)) (X i) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (X i)

Proof state:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
r : R
⊢ (φ.comp (eval₂Hom f g)) (C r) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (C r)

Tactic:
rw [RingHom.comp_apply, eval₂Hom_C, eval₂Hom_C, RingHom.comp_apply]

Result:
no goals

Proof state:
case hX
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
i : σ
⊢ (φ.comp (eval₂Hom f g)) (X i) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (X i)

Tactic:
rw [RingHom.comp_apply, eval₂Hom_X', eval₂Hom_X']

Result:
no goals
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Ico (a b : ℕ) : (↑) '' Ico a b = Ico (a : ℤ) b :=
  (castOrderEmbedding (α := ℤ)).image_Ico (by simp [ordConnected_Ici]) a b

Proof state:
a b : ℕ
⊢ (range ⇑castOrderEmbedding).OrdConnected

Tactic:
simp [ordConnected_Ici]

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
private lemma tendsto_nat_rpow_inv :
    Tendsto (fun k : ℕ ↦ (k : ℝ) ^ (k : ℝ)⁻¹) atTop (𝓝 1)

Proof state:
⊢ Tendsto (fun k => ↑k ^ (↑k)⁻¹) atTop (𝓝 1)

Tactic:
simp_rw [← one_div]

Result:
⊢ Tendsto (fun k => ↑k ^ (1 / ↑k)) atTop (𝓝 1)

Proof state:
⊢ Tendsto (fun k => ↑k ^ (1 / ↑k)) atTop (𝓝 1)

Tactic:
exact Tendsto.comp tendsto_rpow_div tendsto_natCast_atTop_atTop

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem LegendreSym.to_jacobiSym (p : ℕ) (pp : Fact p.Prime) (a r : ℤ)
    (hr : IsInt (jacobiSym a p) r) : IsInt (legendreSym p a) r

Proof state:
p : ℕ
pp : Fact (Nat.Prime p)
a r : ℤ
hr : IsInt (jacobiSym a p) r
⊢ IsInt (legendreSym p a) r

Tactic:
rwa [@jacobiSym.legendreSym.to_jacobiSym p pp a]

Result:
no goals
-- Mathlib/CategoryTheory/Action.lean
lemma cases' ⦃a' b' : ActionCategory G X⦄ (f : a' ⟶ b') :
    ∃ (a b : X) (g : G) (ha : a' = a) (hb : b' = b) (hg : a = g⁻¹ • b),
      f = eqToHom (by rw [ha, hg]) ≫ homOfPair b g ≫ eqToHom (by rw [hb])

Proof state:
X : Type u
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
⊢ ∀ ⦃a' b' : ActionCategory G X⦄ (f : a' ⟶ b'),
    ∃ a b g, ∃ (ha : a' = ⟨(), a⟩) (hb : b' = ⟨(), b⟩) (hg : a = g⁻¹ • b), f = eqToHom ⋯ ≫ homOfPair b g ≫ eqToHom ⋯

Tactic:
exact ActionCategory.cases (fun t g => ⟨g⁻¹ • t, t, g, rfl, rfl, rfl, by simp⟩)

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a' b' : ActionCategory G X
f : a' ⟶ b'
a b : X
g : G
ha : a' = ⟨(), a⟩
hb : b' = ⟨(), b⟩
hg : a = g⁻¹ • b
⊢ ⟨(), b⟩ = b'

Tactic:
rw [hb]

Result:
no goals

Proof state:
X : Type u
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
t : X
g : G
⊢ homOfPair t g = eqToHom ⋯ ≫ homOfPair t g ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a' b' : ActionCategory G X
f : a' ⟶ b'
a b : X
g : G
ha : a' = ⟨(), a⟩
hb : b' = ⟨(), b⟩
hg : a = g⁻¹ • b
⊢ a' = ⟨(), g⁻¹ • b⟩

Tactic:
rw [ha, hg]

Result:
no goals

Proof state:
X : Type u
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a' b' : ActionCategory G X
f : a' ⟶ b'
⊢ ∃ a b g, ∃ (ha : a' = ⟨(), a⟩) (hb : b' = ⟨(), b⟩) (hg : a = g⁻¹ • b), f = eqToHom ⋯ ≫ homOfPair b g ≫ eqToHom ⋯

Tactic:
revert a' b' f

Result:
X : Type u
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
⊢ ∀ ⦃a' b' : ActionCategory G X⦄ (f : a' ⟶ b'),
    ∃ a b g, ∃ (ha : a' = ⟨(), a⟩) (hb : b' = ⟨(), b⟩) (hg : a = g⁻¹ • b), f = eqToHom ⋯ ≫ homOfPair b g ≫ eqToHom ⋯
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem List.trop_sum [AddMonoid R] (l : List R) : trop l.sum = List.prod (l.map trop)

Proof state:
case nil
R : Type u_1
inst✝ : AddMonoid R
⊢ trop [].sum = (map trop []).prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop tl.sum = (map trop tl).prod
⊢ trop (hd :: tl).sum = (map trop (hd :: tl)).prod

Tactic:
simp [← IH]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoid R
l : List R
⊢ trop l.sum = (map trop l).prod

Tactic:
induction' l with hd tl IH

Result:
case nil
R : Type u_1
inst✝ : AddMonoid R
⊢ trop [].sum = (map trop []).prod

case cons
R : Type u_1
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop tl.sum = (map trop tl).prod
⊢ trop (hd :: tl).sum = (map trop (hd :: tl)).prod
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_blsub₂ {o₁ o₂ : Ordinal}
    (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal}
    (ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op

Proof state:
o₁ : Ordinal.{u_4}
o₂ : Ordinal.{u_5}
op : {a : Ordinal.{u_4}} → a < o₁ → {b : Ordinal.{u_5}} → b < o₂ → Ordinal.{max (max u_4 u_5) u_6}
a : Ordinal.{u_4}
b : Ordinal.{u_5}
ha : a < o₁
hb : b < o₂
⊢ b ∈ Iio (type fun x1 x2 => x1 < x2)

Tactic:
rwa [type_lt]

Result:
no goals

Proof state:
o₁ : Ordinal.{u_4}
o₂ : Ordinal.{u_5}
op : {a : Ordinal.{u_4}} → a < o₁ → {b : Ordinal.{u_5}} → b < o₂ → Ordinal.{max (max u_4 u_5) u_6}
a : Ordinal.{u_4}
b : Ordinal.{u_5}
ha : a < o₁
hb : b < o₂
⊢ a ∈ Iio (type fun x1 x2 => x1 < x2)

Tactic:
rwa [type_lt]

Result:
no goals

Proof state:
case h.e'_3
o₁ : Ordinal.{u_4}
o₂ : Ordinal.{u_5}
op : {a : Ordinal.{u_4}} → a < o₁ → {b : Ordinal.{u_5}} → b < o₂ → Ordinal.{max (max u_4 u_5) u_6}
a : Ordinal.{u_4}
b : Ordinal.{u_5}
ha : a < o₁
hb : b < o₂
⊢ op ha hb = (fun {a} => op) ⋯ ⋯

Tactic:
simp only [typein_enum]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma rnDeriv_gaussianReal (μ : ℝ) (v : ℝ≥0) :
    ∂(gaussianReal μ v)/∂volume =ₐₛ gaussianPDF μ v

Proof state:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂ℙ.withDensity (gaussianPDF μ v)/∂ℙ =ᶠ[ae ℙ] gaussianPDF μ v

Tactic:
exact Measure.rnDeriv_withDensity _ (measurable_gaussianPDF μ v)

Result:
no goals

Proof state:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ ∂Measure.dirac μ/∂ℙ =ᶠ[ae ℙ] 0

Tactic:
refine (Measure.eq_rnDeriv measurable_zero (mutuallySingular_dirac μ volume) ?_).symm

Result:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Measure.dirac μ = Measure.dirac μ + ℙ.withDensity 0

Proof state:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae ℙ] gaussianPDF μ v

Tactic:
simp only [hv, gaussianReal_zero_var, gaussianPDF_zero_var]

Result:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ ∂Measure.dirac μ/∂ℙ =ᶠ[ae ℙ] 0

Proof state:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Measure.dirac μ = Measure.dirac μ + ℙ.withDensity 0

Tactic:
rw [withDensity_zero, add_zero]

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae ℙ] gaussianPDF μ v

Tactic:
by_cases hv : v = 0

Result:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae ℙ] gaussianPDF μ v

case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae ℙ] gaussianPDF μ v

Proof state:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae ℙ] gaussianPDF μ v

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv]

Result:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂ℙ.withDensity (gaussianPDF μ v)/∂ℙ =ᶠ[ae ℙ] gaussianPDF μ v
-- Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean
theorem linearIndependent_single {φ : ι → Type*} {f : ∀ ι, φ ι → M}
    (hf : ∀ i, LinearIndependent R (f i)) :
    LinearIndependent R fun ix : Σi, φ i => single ix.1 (f ix.1 ix.2)

Proof state:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ ⨆ a ∈ {i}, LinearMap.range (lsingle a)

Tactic:
rw [span_le]

Result:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(⨆ a ∈ {i}, LinearMap.range (lsingle a))

Proof state:
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (j : ι), LinearIndependent R fun x => single j (f j x)

Tactic:
intro i

Result:
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ LinearIndependent R fun x => single i (f i x)

Proof state:
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
h_disjoint : Disjoint (span R (Set.range (f i))) (ker (lsingle i))
⊢ LinearIndependent R fun x => single i (f i x)

Tactic:
apply (hf i).map h_disjoint

Result:
no goals

Proof state:
case hd
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (i : ι) (t : Set ι),
    t.Finite →
      i ∉ t →
        Disjoint (span R (Set.range fun x => single i (f i x))) (⨆ i ∈ t, span R (Set.range fun x => single i (f i x)))

Tactic:
intro i t _ hit

Result:
case hd
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ Disjoint (span R (Set.range fun x => single i (f i x))) (⨆ i ∈ t, span R (Set.range fun x => single i (f i x)))
-- Mathlib/Data/Set/Card.lean
theorem Finite.encard_lt_top (h : s.Finite) : s.encard < ⊤

Proof state:
α : Type u_1
s : Set α
h : s.Finite
a : α
t : Set α
hat : a ∉ t
hs✝ : t.Finite
ht' : t.encard < ⊤
⊢ (insert a t).encard < ⊤

Tactic:
rw [encard_insert_of_not_mem hat]

Result:
α : Type u_1
s : Set α
h : s.Finite
a : α
t : Set α
hat : a ∉ t
hs✝ : t.Finite
ht' : t.encard < ⊤
⊢ t.encard + 1 < ⊤

Proof state:
α : Type u_1
s : Set α
h : s.Finite
⊢ ∅.encard < ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.Finite
a : α
t : Set α
hat : a ∉ t
hs✝ : t.Finite
ht' : t.encard < ⊤
⊢ t.encard + 1 < ⊤

Tactic:
exact lt_tsub_iff_right.1 ht'

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.Finite
⊢ ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → s.encard < ⊤ → (insert a s).encard < ⊤

Tactic:
rintro a t hat _ ht'

Result:
α : Type u_1
s : Set α
h : s.Finite
a : α
t : Set α
hat : a ∉ t
hs✝ : t.Finite
ht' : t.encard < ⊤
⊢ (insert a t).encard < ⊤

Proof state:
α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard < ⊤

Tactic:
refine h.induction_on _ (by simp) ?_

Result:
α : Type u_1
s : Set α
h : s.Finite
⊢ ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → s.encard < ⊤ → (insert a s).encard < ⊤
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem integral_cos_pow_eq (n : ℕ) :
    (∫ x in (0 : ℝ)..π / 2, cos x ^ n) = 1 / 2 * ∫ x in (0 : ℝ)..π, sin x ^ n

Proof state:
n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n

Tactic:
have R : IntervalIntegrable _ volume (π / 2) π := (continuous_sin.pow n).intervalIntegrable _ _

Result:
n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
lemma comp_C_mul_X_eq_zero_iff {r : R} (hr : r ∈ nonZeroDivisors R) :
    p.comp (C r * X) = 0 ↔ p = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
n : ℕ
⊢ (p.comp (C r * X)).coeff n = coeff 0 n ↔ p.coeff n = coeff 0 n

Tactic:
rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
⊢ p.comp (C r * X) = 0 ↔ p = 0

Tactic:
simp_rw [ext_iff]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
⊢ (∀ (n : ℕ), (p.comp (C r * X)).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), p.coeff n = coeff 0 n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
⊢ (∀ (n : ℕ), (p.comp (C r * X)).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), p.coeff n = coeff 0 n

Tactic:
refine forall_congr' fun n ↦ ?_

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
n : ℕ
⊢ (p.comp (C r * X)).coeff n = coeff 0 n ↔ p.coeff n = coeff 0 n