harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma monomial_mem_coeffsIn : monomial i x ∈ coeffsIn σ M ↔ x ∈ M

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
h : ∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M
⊢ x ∈ M

Tactic:
simpa using h i

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ (monomial i) x ∈ coeffsIn σ M ↔ x ∈ M

Tactic:
classical
simp only [mem_coeffsIn, coeff_monomial]
exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ (monomial i) x ∈ coeffsIn σ M ↔ x ∈ M

Tactic:
simp only [mem_coeffsIn, coeff_monomial]

Result:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M

Tactic:
exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
⊢ (if i = j then x else 0) ∈ M

Tactic:
split <;> simp [hs]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BanachSteinhaus.lean
theorem banach_steinhaus {ι : Type*} [CompleteSpace E] {g : ι → E →SL[σ₁₂] F}
    (h : ∀ x, ∃ C, ∀ i, ‖g i x‖ ≤ C) : ∃ C', ∀ i, ‖g i‖ ≤ C'

Proof state:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C
⊢ UniformEquicontinuous (DFunLike.coe ∘ g)

Tactic:
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)

Result:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C
x✝ : Fin 1
x : E
⊢ BddAbove (range fun i => (normSeminorm 𝕜₂ F) ((g i) x))

Proof state:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C
⊢ ∃ C', ∀ (i : ι), ‖g i‖ ≤ C'

Tactic:
rw [show (∃ C, ∀ i, ‖g i‖ ≤ C) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 5 2]

Result:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C
⊢ UniformEquicontinuous (DFunLike.coe ∘ g)

Proof state:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C
x✝ : Fin 1
x : E
⊢ BddAbove (range fun i => (normSeminorm 𝕜₂ F) ((g i) x))

Tactic:
simpa [bddAbove_def, forall_mem_range] using h x

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left (x y z : E) : inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
H_re :
  -(‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) + (‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) +
        (‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖) -
      (‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) =
    -(2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)) + 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖) +
        2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) -
      2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
H_im :
  -(‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖) +
          (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) +
        (‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖) -
      (‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) =
    -(2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)) +
          2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖) +
        2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) -
      2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
H :
  -(𝓚 ‖2 • x + y‖ * 𝓚 ‖2 • x + y‖ + 𝓚 ‖2 • z + y‖ * 𝓚 ‖2 • z + y‖) +
            (𝓚 ‖2 • x + y‖ * 𝓚 ‖2 • x + y‖ + 𝓚 ‖y - 2 • z‖ * 𝓚 ‖y - 2 • z‖) +
          (𝓚 ‖2 • z + y‖ * 𝓚 ‖2 • z + y‖ + 𝓚 ‖y‖ * 𝓚 ‖y‖) -
        (𝓚 ‖y‖ * 𝓚 ‖y‖ + 𝓚 ‖y - 2 • z‖ * 𝓚 ‖y - 2 • z‖) +
      I *
        (-(𝓚 ‖I • (2 • x + y)‖ * 𝓚 ‖I • (2 • x + y)‖ + 𝓚 ‖I • y + 2 • z‖ * 𝓚 ‖I • y + 2 • z‖) +
              (𝓚 ‖I • (2 • x + y)‖ * 𝓚 ‖I • (2 • x + y)‖ + 𝓚 ‖I • y - 2 • z‖ * 𝓚 ‖I • y - 2 • z‖) +
            (𝓚 ‖I • y + 2 • z‖ * 𝓚 ‖I • y + 2 • z‖ + 𝓚 ‖I • y‖ * 𝓚 ‖I • y‖) -
          (𝓚 ‖I • y‖ * 𝓚 ‖I • y‖ + 𝓚 ‖I • y - 2 • z‖ * 𝓚 ‖I • y - 2 • z‖)) =
    -(2 * (𝓚 ‖x + y + z‖ * 𝓚 ‖x + y + z‖ + 𝓚 ‖x - z‖ * 𝓚 ‖x - z‖)) +
            2 * (𝓚 ‖x + y - z‖ * 𝓚 ‖x + y - z‖ + 𝓚 ‖x + z‖ * 𝓚 ‖x + z‖) +
          2 * (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖) -
        2 * (𝓚 ‖y - z‖ * 𝓚 ‖y - z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖) +
      I *
        (-(2 * (𝓚 ‖I • (x + y) + z‖ * 𝓚 ‖I • (x + y) + z‖ + 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖)) +
              2 * (𝓚 ‖I • (x + y) - z‖ * 𝓚 ‖I • (x + y) - z‖ + 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖) +
            2 * (𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖) -
          2 * (𝓚 ‖I • y - z‖ * 𝓚 ‖I • y - z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖))
⊢ 4⁻¹ *
      (𝓚 ‖x + y + z‖ * 𝓚 ‖x + y + z‖ - 𝓚 ‖x + y - z‖ * 𝓚 ‖x + y - z‖ + I * 𝓚 ‖I • (x + y) + z‖ * 𝓚 ‖I • (x + y) + z‖ -
        I * 𝓚 ‖I • (x + y) - z‖ * 𝓚 ‖I • (x + y) - z‖) =
    4⁻¹ *
        (𝓚 ‖x + z‖ * 𝓚 ‖x + z‖ - 𝓚 ‖x - z‖ * 𝓚 ‖x - z‖ + I * 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖ -
          I * 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖) +
      4⁻¹ *
        (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ - 𝓚 ‖y - z‖ * 𝓚 ‖y - z‖ + I * 𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ -
          I * 𝓚 ‖I • y - z‖ * 𝓚 ‖I • y - z‖)

Tactic:
linear_combination H / 8

Result:
no goals
-- Mathlib/RingTheory/Filtration.lean
theorem _root_.Ideal.stableFiltration_stable (I : Ideal R) (N : Submodule R M) :
    (I.stableFiltration N).Stable

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)

Tactic:
dsimp

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
⊢ (I.stableFiltration N).Stable

Tactic:
use 0

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
⊢ ∀ n ≥ 0, I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N

Tactic:
rw [add_comm, pow_add, mul_smul, pow_one]

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
⊢ ∀ n ≥ 0, I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)

Tactic:
intro n _

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma IsBlock.disjoint_smul_set_smul (hB : IsBlock G B) (hgs : ¬ g • B ⊆ s • B) :
    Disjoint (g • B) (s • B)

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ Disjoint (g • B) (s • B)

Tactic:
rw [← iUnion_smul_set, disjoint_iUnion₂_right]

Result:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ ∀ i ∈ s, Disjoint (g • B) (i • B)

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ ∀ i ∈ s, Disjoint (g • B) (i • B)

Tactic:
exact fun b hb ↦ hB fun h ↦ hgs <| h.trans_subset <| smul_set_subset_smul hb

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem Scheme.homOfLE_base {U V : X.Opens} (e : U ≤ V) :
    (X.homOfLE e).base = (Opens.toTopCat _).map (homOfLE e)

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (X.homOfLE e).base = (Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e)

Tactic:
ext a

Result:
case w
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↑↑(↑U).toPresheafedSpace
⊢ (ConcreteCategory.hom (X.homOfLE e).base) a =
    (ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) a

Proof state:
case w
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↑↑(↑U).toPresheafedSpace
⊢ (ConcreteCategory.hom (X.homOfLE e).base) a =
    (ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) a

Tactic:
refine Subtype.ext ?_

Result:
case w
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↑↑(↑U).toPresheafedSpace
⊢ ↑((ConcreteCategory.hom (X.homOfLE e).base) a) =
    ↑((ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) a)

Proof state:
case w
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↑↑(↑U).toPresheafedSpace
⊢ ↑((ConcreteCategory.hom (X.homOfLE e).base) a) =
    ↑((ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) a)

Tactic:
exact congr($(X.homOfLE_ι e).base a)

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
private lemma supDegree_monic_esymm [Nontrivial R] {i : ℕ} (him : i < m) :
    supDegree toLex (esymm (Fin m) R (i + 1)) =
      toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun _ _ ↦ 1) ∧
    Monic toLex (esymm (Fin m) R (i + 1))

Proof state:
case refine_3
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
this :
  supDegree (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      supDegree (⇑toLex) ((monomial (∑ j ∈ Iic ⟨i, him⟩, fun₀ | j => 1)) 1) ∧
    leadingCoeff (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      leadingCoeff (⇑toLex) ((monomial (∑ j ∈ Iic ⟨i, him⟩, fun₀ | j => 1)) 1)
⊢ supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1) ∧
    Monic (⇑toLex) (esymm (Fin m) R (i + 1))

Tactic:
rwa [← esymm_eq_sum_monomial, ← Finsupp.indicator_eq_sum_single, ← single_eq_monomial,
  supDegree_single_ne_zero _ one_ne_zero, leadingCoeff_single toLex.injective] at this

Result:
no goals

Proof state:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
⊢ toLex (Finsupp.indicator t fun x x => 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1)

Tactic:
have hkm := mem_sdiff.1 (min'_mem _ hne)

Result:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ toLex (Finsupp.indicator t fun x x => 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) :
    (l.set n a).take m = l.take m :=
  List.ext_getElem? fun i => by
    rw [getElem?_take, getElem?_take]
    split
    · next h' => rw [getElem?_set_ne (by omega)]
    · rfl

Proof state:
case isFalse
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
h✝ : ¬i < m
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
h' : i < m
⊢ (l.set n a)[i]? = l[i]?

Tactic:
rw [getElem?_set_ne (by omega)]

Result:
no goals

Proof state:
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
h' : i < m
⊢ n ≠ i

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
h✝ : i < m
⊢ (l.set n a)[i]? = l[i]?

Tactic:
next h' => rw [getElem?_set_ne (by omega)]

Result:
no goals

Proof state:
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
⊢ (if i < m then (l.set n a)[i]? else none) = if i < m then l[i]? else none

Tactic:
split

Result:
case isTrue
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
h✝ : i < m
⊢ (l.set n a)[i]? = l[i]?

case isFalse
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
h✝ : ¬i < m
⊢ none = none

Proof state:
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
⊢ (take m (l.set n a))[i]? = (take m l)[i]?

Tactic:
rw [getElem?_take, getElem?_take]

Result:
α : Type u_1
a : α
n m : Nat
l : List α
h : m < n
i : Nat
⊢ (if i < m then (l.set n a)[i]? else none) = if i < m then l[i]? else none
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_lt (hx : y ≤ x) (hy : y ≠ ⊥) : x \ y < x

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
⊢ x \ y < x

Tactic:
refine sdiff_le.lt_of_ne fun h => hy ?_

Result:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ y = ⊥

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ y = ⊥

Tactic:
rw [sdiff_eq_self_iff_disjoint', disjoint_iff] at h

Result:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥

Tactic:
rw [← h, inf_eq_right.mpr hx]

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma negOnePow_eq_neg_one_iff (n : ℤ) : n.negOnePow = -1 ↔ Odd n

Proof state:
case mp
n : ℤ
h : n.negOnePow = -1
⊢ Odd n

Tactic:
rw [← Int.not_even_iff_odd]

Result:
case mp
n : ℤ
h : n.negOnePow = -1
⊢ ¬Even n

Proof state:
case mp
n : ℤ
h : n.negOnePow = -1
h' : Even n
⊢ False

Tactic:
rw [negOnePow_even _ h'] at h

Result:
case mp
n : ℤ
h : 1 = -1
h' : Even n
⊢ False

Proof state:
n : ℤ
⊢ n.negOnePow = -1 ↔ Odd n

Tactic:
constructor

Result:
case mp
n : ℤ
⊢ n.negOnePow = -1 → Odd n

case mpr
n : ℤ
⊢ Odd n → n.negOnePow = -1

Proof state:
case mpr
n : ℤ
⊢ Odd n → n.negOnePow = -1

Tactic:
exact negOnePow_odd n

Result:
no goals

Proof state:
case mp
n : ℤ
⊢ n.negOnePow = -1 → Odd n

Tactic:
intro h

Result:
case mp
n : ℤ
h : n.negOnePow = -1
⊢ Odd n

Proof state:
case mp
n : ℤ
h : n.negOnePow = -1
⊢ ¬Even n

Tactic:
intro h'

Result:
case mp
n : ℤ
h : n.negOnePow = -1
h' : Even n
⊢ False

Proof state:
case mp
n : ℤ
h : 1 = -1
h' : Even n
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem comp_mul_left (x y : α) : (x * ·) ∘ (y * ·) = (x * y * ·)

Proof state:
α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) = fun x_1 => x * y * x_1

Tactic:
ext z

Result:
case h
α : Type u_1
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) z = x * y * z

Proof state:
case h
α : Type u_1
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) z = x * y * z

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem floor_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / (↑d : ℤ)

Proof state:
case inl
n : ℤ
⊢ (↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0

Tactic:
simp

Result:
no goals

Proof state:
n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d

Tactic:
obtain rfl | hd := eq_zero_or_pos (a := d)

Result:
case inl
n : ℤ
⊢ (↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0

case inr
n : ℤ
d : ℕ
hd : 0 < d
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d

Proof state:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den

Tactic:
exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

Result:
no goals

Proof state:
case inr.intro.intro
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = c * q.num / (c * ↑q.den)

Tactic:
refine (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left ?_ <| Int.natCast_nonneg q.den).symm

Result:
case inr.intro.intro
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < c * ↑q.den

Proof state:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ q.num / ↑q.den = n / ↑d

Tactic:
obtain ⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩ : ∃ c, n = c * q.num ∧ (d : ℤ) = c * q.den := by
  rw [q_eq]
  exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

Result:
case inr.intro.intro
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = n / ↑d

Proof state:
case inr.intro.intro
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = n / ↑d

Tactic:
rw [n_eq_c_mul_num, d_eq_c_mul_denom]

Result:
case inr.intro.intro
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = c * q.num / (c * ↑q.den)

Proof state:
case inr.intro.intro
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < c * ↑q.den

Tactic:
rwa [← d_eq_c_mul_denom, Int.natCast_pos]

Result:
no goals

Proof state:
n : ℤ
d : ℕ
⊢ ⌊↑n / ↑d⌋ = n / ↑d

Tactic:
rw [Rat.floor_def]

Result:
n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d

Proof state:
case inr
n : ℤ
d : ℕ
hd : 0 < d
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d

Tactic:
set q := (n : ℚ) / d with q_eq

Result:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ q.num / ↑q.den = n / ↑d

Proof state:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * q.num ∧ ↑d = c * ↑q.den

Tactic:
rw [q_eq]

Result:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
@[simp]
lemma klDiv_self (μ : Measure α) [SigmaFinite μ] : klDiv μ μ = 0

Proof state:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ μ ≪ μ ∧ Integrable (llr μ μ) μ

Tactic:
rw [integrable_congr h]

Result:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ μ ≪ μ ∧ Integrable 0 μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ klDiv μ μ = 0

Tactic:
rw [klDiv_def, if_pos]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + (μ univ).toReal - (μ univ).toReal) = 0

case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ μ ≪ μ ∧ Integrable (llr μ μ) μ

Proof state:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ μ ≪ μ ∧ Integrable 0 μ

Tactic:
exact ⟨Measure.AbsolutelyContinuous.rfl, integrable_zero _ _ μ⟩

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ klDiv μ μ = 0

Tactic:
have h := llr_self μ

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ klDiv μ μ = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + (μ univ).toReal - (μ univ).toReal) = 0

Tactic:
simp [integral_congr_ae h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.zero_ult' (a : BitVec w) : (BitVec.ult 0#w a) = (!a == 0#w)

Proof state:
w : Nat
a : BitVec w
this : (0#w).ult a = true ↔ a ≠ 0#w
h : (0#w).ult a = false
⊢ false = !a == 0#w

Tactic:
simp_all

Result:
no goals

Proof state:
w : Nat
a : BitVec w
this : (0#w).ult a = true ↔ a ≠ 0#w
h : (0#w).ult a = true
⊢ true = !a == 0#w

Tactic:
simp_all

Result:
no goals

Proof state:
w : Nat
a : BitVec w
this : (0#w).ult a = true ↔ a ≠ 0#w
⊢ (0#w).ult a = !a == 0#w

Tactic:
match h:BitVec.ult 0#w a with
| true => simp_all
| false => simp_all

Result:
no goals

Proof state:
w : Nat
a : BitVec w
this : 0#w < a ↔ a ≠ 0#w
⊢ (0#w).ult a = !a == 0#w

Tactic:
rw [BitVec.lt_ult] at this

Result:
w : Nat
a : BitVec w
this : (0#w).ult a = true ↔ a ≠ 0#w
⊢ (0#w).ult a = !a == 0#w

Proof state:
w : Nat
a : BitVec w
⊢ (0#w).ult a = !a == 0#w

Tactic:
have := BitVec.zero_lt_iff_zero_neq a

Result:
w : Nat
a : BitVec w
this : 0#w < a ↔ a ≠ 0#w
⊢ (0#w).ult a = !a == 0#w
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < π / 2) : 0 < tan x

Proof state:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ -(π / 2) < x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < sin x / cos x

Tactic:
exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith)) (cos_pos_of_mem_Ioo ⟨by linarith, hxp⟩)

Result:
no goals

Proof state:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ x < π

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < tan x

Tactic:
rw [tan_eq_sin_div_cos]

Result:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < sin x / cos x