harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/AEDisjoint.lean
theorem union_left_iff : AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u

Tactic:
simp [union_eq_iUnion, and_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_add {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
    W.Nonsingular <| W.add P Q

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ W.Nonsingular (W.add P Q)

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ W.Nonsingular (W.add P Q)

Tactic:
simp only [add_of_Z_eq_zero hP hQ hPz hQz,
  nonsingular_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, nonsingular_zero]

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ W.Nonsingular (W.add P Q)

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
⊢ W.Nonsingular (W.add P Q)
-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma EssFiniteType.comp [h₁ : EssFiniteType R S] [h₂ : EssFiniteType S T] :
    EssFiniteType R T

Proof state:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
⊢ ∀ (s_1 : T),
    ∃ t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t,
      IsUnit t_1 ∧ s_1 * t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
intro x

Result:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x : T
⊢ ∃ t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t,
    IsUnit t_1 ∧ x * t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem find?_eq_find?_finRange {p : Fin n → Bool} : find? p = (List.finRange n).find? p

Proof state:
case succ
n : Nat
ih : ∀ {p : Fin n → Bool}, find? p = List.find? p (List.finRange n)
p : Fin (n + 1) → Bool
⊢ (if p 0 = true then some 0 else Option.map succ (find? fun i => p i.succ)) =
    match p 0 with
    | true => some 0
    | false => List.find? p (List.map succ (List.finRange n))

Tactic:
split <;> simp [Function.comp_def, *]

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ {p : Fin n → Bool}, find? p = List.find? p (List.finRange n)
p : Fin (n + 1) → Bool
⊢ find? p = List.find? p (List.finRange (n + 1))

Tactic:
rw [find?_succ, List.finRange_succ, List.find?_cons]

Result:
case succ
n : Nat
ih : ∀ {p : Fin n → Bool}, find? p = List.find? p (List.finRange n)
p : Fin (n + 1) → Bool
⊢ (if p 0 = true then some 0 else Option.map succ (find? fun i => p i.succ)) =
    match p 0 with
    | true => some 0
    | false => List.find? p (List.map succ (List.finRange n))

Proof state:
n : Nat
p : Fin n → Bool
⊢ find? p = List.find? p (List.finRange n)

Tactic:
induction n with
| zero => rfl
| succ n ih =>
  rw [find?_succ, List.finRange_succ, List.find?_cons]
  split <;> simp [Function.comp_def, *]

Result:
no goals

Proof state:
case zero
p : Fin 0 → Bool
⊢ find? p = List.find? p (List.finRange 0)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem hasUnitMulPowIrreducibleFactorization :
    HasUnitMulPowIrreducibleFactorization k⟦X⟧ :=
  ⟨X, And.intro X_irreducible
      (by
        intro f hf
        use f.order.lift (order_finite_iff_ne_zero.mpr hf)
        use Unit_of_divided_by_X_pow_order f
        simp only [Unit_of_divided_by_X_pow_order_nonzero hf]
        exact self_eq_X_pow_order_mul_divided_by_X_pow_order hf)⟩

Proof state:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ X ^ f.order.lift ⋯ * divided_by_X_pow_order hf = f

Tactic:
exact self_eq_X_pow_order_mul_divided_by_X_pow_order hf

Result:
no goals

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ∃ n, Associated (X ^ n) f

Tactic:
use f.order.lift (order_finite_iff_ne_zero.mpr hf)

Result:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Associated (X ^ f.order.lift ⋯) f

Proof state:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Associated (X ^ f.order.lift ⋯) f

Tactic:
use Unit_of_divided_by_X_pow_order f

Result:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ X ^ f.order.lift ⋯ * ↑f.Unit_of_divided_by_X_pow_order = f

Proof state:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ X ^ f.order.lift ⋯ * ↑f.Unit_of_divided_by_X_pow_order = f

Tactic:
simp only [Unit_of_divided_by_X_pow_order_nonzero hf]

Result:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ X ^ f.order.lift ⋯ * divided_by_X_pow_order hf = f

Proof state:
k : Type u_2
inst✝ : Field k
⊢ ∀ {x : k⟦X⟧}, x ≠ 0 → ∃ n, Associated (X ^ n) x

Tactic:
intro f hf

Result:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ∃ n, Associated (X ^ n) f
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_prod [IsDomain R] {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι}
    (H : ∀ i ∈ s, P i ≠ 0) :
    m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Proof state:
case H.a0
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
i : ι
hi : i ∈ s
⊢ m.leadingCoeff (P i) ≠ 0

Tactic:
rw [leadingCoeff_ne_zero_iff]

Result:
case H.a0
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
i : ι
hi : i ∈ s
⊢ P i ≠ 0

Proof state:
case H
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))

Tactic:
intro i hi

Result:
case H
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
i : ι
hi : i ∈ s
⊢ IsRegular (m.leadingCoeff (P i))

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
apply degree_prod_of_regular

Result:
case H
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))

Proof state:
case H.a0
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
i : ι
hi : i ∈ s
⊢ P i ≠ 0

Tactic:
exact H i hi

Result:
no goals

Proof state:
case H
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
i : ι
hi : i ∈ s
⊢ IsRegular (m.leadingCoeff (P i))

Tactic:
apply isRegular_of_ne_zero

Result:
case H.a0
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
i : ι
hi : i ∈ s
⊢ m.leadingCoeff (P i) ≠ 0
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem mk_smul (c : R) (p q : K[X]) : RatFunc.mk (c • p) q = c • RatFunc.mk p q

Proof state:
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
letI : SMulZeroClass R (FractionRing K[X]) := inferInstance

Result:
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Proof state:
case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]

Result:
no goals

Proof state:
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
by_cases hq : q = 0

Result:
case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Proof state:
case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
  ofFractionRing_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem LinearIndepOn.insert (hs : LinearIndepOn K id s) (hx : x ∉ span K s) :
    LinearIndepOn K id (insert x s)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
⊢ LinearIndepOn K id (insert x s)

Tactic:
rw [← union_singleton]

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
⊢ LinearIndepOn K id (s ∪ {x})

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
x0 : x ≠ 0
⊢ LinearIndepOn K id (s ∪ {x})

Tactic:
apply hs.id_union (LinearIndepOn.singleton x0)

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
x0 : x ≠ 0
⊢ Disjoint (span K s) (span K {x})

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
⊢ LinearIndepOn K id (s ∪ {x})

Tactic:
have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem (span K s)) hx

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
x0 : x ≠ 0
⊢ LinearIndepOn K id (s ∪ {x})

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
x0 : x ≠ 0
⊢ Disjoint (span K s) (span K {x})

Tactic:
rwa [disjoint_span_singleton' x0]

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
⊢ x = 0 → x ∈ span K s

Tactic:
rintro rfl

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
hs : LinearIndepOn K id s
hx : 0 ∉ span K s
⊢ 0 ∈ span K s

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
hs : LinearIndepOn K id s
hx : 0 ∉ span K s
⊢ 0 ∈ span K s

Tactic:
apply zero_mem (span K s)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp]
lemma card_smul_expect (s : Finset ι) (f : ι → M) : #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Proof state:
case inr.ha
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ ↑(#s) ≠ 0

Tactic:
exact mod_cast hs.card_ne_zero

Result:
no goals

Proof state:
case inl
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ #∅ • 𝔼 i ∈ ∅, f i = ∑ i ∈ ∅, f i

Tactic:
simp

Result:
no goals

Proof state:
case inr
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]

Result:
case inr.ha
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ ↑(#s) ≠ 0

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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ #∅ • 𝔼 i ∈ ∅, f i = ∑ i ∈ ∅, f i

case inr
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma IccLeftChart_extend_bot_mem_frontier :
    (IccLeftChart x y).extend (𝓡∂ 1) ⊥ ∈ frontier (range (𝓡∂ 1))

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) ⊥ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
  mem_setOf, PiLp.zero_apply]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_eq_bot (a b : EReal) :
    a * b = ⊥ ↔ (a = ⊥ ∧ 0 < b) ∨ (0 < a ∧ b = ⊥) ∨ (a = ⊤ ∧ b < 0) ∨ (a < 0 ∧ b = ⊤)

Proof state:
a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ 0 < a ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ a < 0 ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
tauto

Result:
no goals

Proof state:
a b : EReal
⊢ a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
rw [← neg_eq_top_iff, ← EReal.neg_mul, mul_eq_top, neg_eq_bot_iff, neg_eq_top_iff,
  neg_lt_comm, lt_neg_comm, neg_zero]

Result:
a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ 0 < a ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ a < 0 ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem edist_toL1_toL1 (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) :
    edist (hf.toL1 f) (hg.toL1 g) = ∫⁻ a, edist (f a) (g a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ (if 1 = ⊤ then eLpNormEssSup (f - g) μ else ∫⁻ (a : α), ‖f a - g a‖ₑ ∂μ) = ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
simp [edist_eq_enorm_sub]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ edist (toL1 f hf) (toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
simp only [toL1, Lp.edist_toLp_toLp, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm,
  Pi.sub_apply, one_toReal, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ (if 1 = ⊤ then eLpNormEssSup (f - g) μ else ∫⁻ (a : α), ‖f a - g a‖ₑ ∂μ) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem measurable_dirac : Measurable (Measure.dirac : α → Measure α)

Proof state:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => (dirac b) s

Tactic:
simp_rw [dirac_apply' _ hs]

Result:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => s.indicator 1 b

Proof state:
α : Type u_1
mα : MeasurableSpace α
⊢ Measurable dirac

Tactic:
refine measurable_of_measurable_coe _ fun s hs => ?_

Result:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => (dirac b) s

Proof state:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => s.indicator 1 b

Tactic:
exact measurable_one.indicator hs

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma isoClosure_le_iff (P Q : MorphismProperty C) [Q.RespectsIso] :
    P.isoClosure ≤ Q ↔ P ≤ Q

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P.isoClosure ≤ Q → P ≤ Q

Tactic:
exact P.le_isoClosure.trans

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ P.isoClosure ≤ Q

Tactic:
exact (monotone_isoClosure h).trans (by rw [Q.isoClosure_eq_self])

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ Q.isoClosure ≤ Q

Tactic:
rw [Q.isoClosure_eq_self]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P.isoClosure ≤ Q ↔ P ≤ Q

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P.isoClosure ≤ Q → P ≤ Q

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P ≤ Q → P.isoClosure ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P ≤ Q → P.isoClosure ≤ Q

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ P.isoClosure ≤ Q
-- Mathlib/CategoryTheory/Limits/IsConnected.lean
theorem isConnected_iff_of_initial (F : C ⥤ D) [F.Initial] : IsConnected C ↔ IsConnected D

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Initial
⊢ IsConnected C ↔ IsConnected D

Tactic:
rw [← isConnected_op_iff_isConnected C, ← isConnected_op_iff_isConnected D]

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Initial
⊢ IsConnected Cᵒᵖ ↔ IsConnected Dᵒᵖ

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Initial
⊢ IsConnected Cᵒᵖ ↔ IsConnected Dᵒᵖ

Tactic:
exact isConnected_iff_of_final F.op

Result:
no goals
-- Mathlib/Data/Set/Equitable.lean
theorem equitableOn_iff :
    EquitableOn (s : Set α) f ↔
      ∀ a ∈ s, f a = (∑ i ∈ s, f i) / s.card ∨ f a = (∑ i ∈ s, f i) / s.card + 1

Proof state:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (↑s).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / #s ∨ f a = (∑ i ∈ s, f i) / #s + 1

Tactic:
simp_rw [equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem lowerCrossingTime_le_upperCrossingTime_succ :
    lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω

Tactic:
rw [upperCrossingTime_succ]

Result:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤
    hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤
    hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Tactic:
exact le_hitting lowerCrossingTime_le ω

Result:
no goals
-- Mathlib/FieldTheory/KummerPolynomial.lean
lemma ne_zero_of_irreducible_X_pow_sub_C' {n : ℕ} (hn : n ≠ 1) {a : K}
    (H : Irreducible (X ^ n - C a)) : a ≠ 0

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
a : K
H : Irreducible (X ^ n - C a)
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n - C 0)
⊢ False

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n - C 0)
⊢ False

Tactic:
rw [map_zero, sub_zero] at H

Result:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n)
⊢ False

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n)
⊢ False

Tactic:
exact not_irreducible_pow hn H

Result:
no goals