harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem ite_none_right_eq_some {p : Prop} [Decidable p] {b : Option α} :
    (if p then b else none) = some a ↔ p ∧ b = some a

Proof state:
α : Type u_1
a : α
p : Prop
inst✝ : Decidable p
b : Option α
⊢ (if p then b else none) = some a ↔ p ∧ b = some a

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem left_dist_ne_zero_of_angle_eq_pi {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π) : dist p₁ p₂ ≠ 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ dist p₁ p₂ ≠ 0

Tactic:
by_contra heq

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : dist p₁ p₂ = 0
⊢ False

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : p₁ = p₂
⊢ False

Tactic:
rw [heq, angle_self_left] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : π / 2 = π
heq : p₁ = p₂
⊢ False

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : π / 2 = π
heq : p₁ = p₂
⊢ False

Tactic:
exact Real.pi_ne_zero (by linarith)

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : π / 2 = π
heq : p₁ = p₂
⊢ π = 0

Tactic:
linarith

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : dist p₁ p₂ = 0
⊢ False

Tactic:
rw [dist_eq_zero] at heq

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : p₁ = p₂
⊢ False
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem leftDistributor_ext₂_left {J : Type} [Fintype J]
    {X Y Z : C} {f : J → C} {g h : X ⊗ (Y ⊗ ⨁ f) ⟶ Z}
    (w : ∀ j, (X ◁ (Y ◁ biproduct.ι f j)) ≫ g = (X ◁ (Y ◁ biproduct.ι f j)) ≫ h) :
    g = h

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
⊢ g = h

Tactic:
apply (cancel_epi (α_ _ _ _).hom).mp

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
⊢ (α_ X Y (⨁ f)).hom ≫ g = (α_ X Y (⨁ f)).hom ≫ h

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
j✝ : J
⊢ (X ⊗ Y) ◁ biproduct.ι f j✝ ≫ (α_ X Y (⨁ f)).hom ≫ g = (X ⊗ Y) ◁ biproduct.ι f j✝ ≫ (α_ X Y (⨁ f)).hom ≫ h

Tactic:
simp [w]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
⊢ (α_ X Y (⨁ f)).hom ≫ g = (α_ X Y (⨁ f)).hom ≫ h

Tactic:
ext

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
j✝ : J
⊢ (X ⊗ Y) ◁ biproduct.ι f j✝ ≫ (α_ X Y (⨁ f)).hom ≫ g = (X ⊗ Y) ◁ biproduct.ι f j✝ ≫ (α_ X Y (⨁ f)).hom ≫ h
-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_toPEquiv_apply [DecidableEq n] [Zero α] [One α] (f : m ≃ n) (i) :
    f.toPEquiv.toMatrix i = Pi.single (f i) (1 : α)

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
i : m
⊢ f.toPEquiv.toMatrix i = Pi.single (f i) 1

Tactic:
ext

Result:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
i : m
x✝ : n
⊢ f.toPEquiv.toMatrix i x✝ = Pi.single (f i) 1 x✝

Proof state:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
i : m
x✝ : n
⊢ f.toPEquiv.toMatrix i x✝ = Pi.single (f i) 1 x✝

Tactic:
simp [toMatrix_apply, Pi.single_apply, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
@[reassoc]
lemma totalFlipIsoX_hom_D₁ (j j' : J) :
    (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' =
      K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom

Proof state:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
ext i₂ i₁ h₁

Result:
case pos.h
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
⊢ K.flip.ιTotal c i₂ i₁ j h₁ ≫ (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' =
    K.flip.ιTotal c i₂ i₁ j h₁ ≫ K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_intMin {w : Nat} :
    (intMin w).toInt = -((2 ^ (w - 1) % 2 ^ w) : Nat)

Proof state:
case neg
w : Nat
h : ¬w = 0
w_pos : 0 < w
⊢ 2 * 2 ^ (w - 1) < 2 ^ w → ↑(2 ^ (w - 1)) = -↑(2 ^ (w - 1))

Tactic:
rw [Nat.mul_comm]

Result:
case neg
w : Nat
h : ¬w = 0
w_pos : 0 < w
⊢ 2 ^ (w - 1) * 2 < 2 ^ w → ↑(2 ^ (w - 1)) = -↑(2 ^ (w - 1))

Proof state:
w : Nat
⊢ (intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

Tactic:
by_cases h : w = 0

Result:
case pos
w : Nat
h : w = 0
⊢ (intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

case neg
w : Nat
h : ¬w = 0
⊢ (intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

Proof state:
case neg
w : Nat
h : ¬w = 0
⊢ (intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

Tactic:
have w_pos : 0 < w := by omega

Result:
case neg
w : Nat
h : ¬w = 0
w_pos : 0 < w
⊢ (intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

Proof state:
case neg
w : Nat
h : ¬w = 0
w_pos : 0 < w
⊢ (intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

Tactic:
simp only [BitVec.toInt, toNat_intMin, w_pos, Nat.two_pow_pred_mod_two_pow,
  Int.two_pow_pred_sub_two_pow, ite_eq_right_iff]

Result:
case neg
w : Nat
h : ¬w = 0
w_pos : 0 < w
⊢ 2 * 2 ^ (w - 1) < 2 ^ w → ↑(2 ^ (w - 1)) = -↑(2 ^ (w - 1))

Proof state:
case pos
w : Nat
h : w = 0
⊢ (intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

Tactic:
subst h

Result:
case pos

⊢ (intMin 0).toInt = -↑(2 ^ (0 - 1) % 2 ^ 0)

Proof state:
case pos

⊢ (intMin 0).toInt = -↑(2 ^ (0 - 1) % 2 ^ 0)

Tactic:
simp [BitVec.toInt]

Result:
no goals

Proof state:
case neg
w : Nat
h : ¬w = 0
w_pos : 0 < w
⊢ 2 ^ (w - 1) * 2 < 2 ^ w → ↑(2 ^ (w - 1)) = -↑(2 ^ (w - 1))

Tactic:
simp [w_pos]

Result:
no goals

Proof state:
w : Nat
h : ¬w = 0
⊢ 0 < w

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_iff_integrableOn_Ioo_of_le [NoAtoms μ] (hab : a ≤ b) :
    IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioo a b) μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
inst✝ : NoAtoms μ
hab : a ≤ b
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioo]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y)

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ y = 0#1 ∨ y = 1#1

Tactic:
bv_omega

Result:
no goals

Proof state:
x y : BitVec 1
⊢ x = 0#1 ∨ x = 1#1

Tactic:
bv_omega

Result:
no goals

Proof state:
x y : BitVec 1
⊢ x % y = x &&& ~~~y

Tactic:
have hx : x = 0#1 ∨ x = 1#1 := by bv_omega

Result:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ x % y = x &&& ~~~y

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ x % y = x &&& ~~~y

Tactic:
have hy : y = 0#1 ∨ y = 1#1 := by bv_omega

Result:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
hy : y = 0#1 ∨ y = 1#1
⊢ x % y = x &&& ~~~y

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
hy : y = 0#1 ∨ y = 1#1
⊢ x % y = x &&& ~~~y

Tactic:
rcases hx with rfl | rfl <;>
  rcases hy with rfl | rfl <;>
    rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_nonsingular (hf : Function.Injective f) (P : Fin 3 → R) :
    (W'.map f).toProjective.Nonsingular (f ∘ P) ↔ W'.Nonsingular P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (map W' f).toProjective.Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P

Tactic:
simp only [Nonsingular, map_equation hf, map_polynomialX, map_polynomialY, map_polynomialZ,
  eval_map, ← eval₂_comp, map_ne_zero_iff f hf]

Result:
no goals
-- Mathlib/RingTheory/FiniteStability.lean
theorem baseChangeAux_surj {σ : Type*} {f : MvPolynomial σ R →ₐ[R] A} (hf : Function.Surjective f) :
    Function.Surjective (Algebra.TensorProduct.map (AlgHom.id B B) f)

Proof state:
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(TensorProduct.map (AlgHom.id R B) f)

Tactic:
apply TensorProduct.map_surjective

Result:
case hg
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(AlgHom.id R B).toLinearMap

case hg'
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑f.toLinearMap

Proof state:
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(TensorProduct.map (AlgHom.id B B) f)

Tactic:
show Function.Surjective (TensorProduct.map (AlgHom.id R B) f)

Result:
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(TensorProduct.map (AlgHom.id R B) f)

Proof state:
case hg'
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑f.toLinearMap

Tactic:
exact hf

Result:
no goals

Proof state:
case hg
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(AlgHom.id R B).toLinearMap

Tactic:
exact Function.RightInverse.surjective (congrFun rfl)

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem fst_isOpenEmbedding_of_right {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S}
    (H : IsOpenEmbedding g) : IsOpenEmbedding <| ⇑(pullback.fst f g)

Proof state:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ ⇑(ConcreteCategory.hom (pullback.fst f g)) =
    ⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯))

Tactic:
simp [homeoOfIso, ← coe_comp]

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
convert (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isOpenEmbedding.comp
    (pullback_map_isOpenEmbedding (i₁ := 𝟙 X) f g f (𝟙 _)
      (homeoOfIso (Iso.refl _)).isOpenEmbedding H (𝟙 _) rfl (by simp))

Result:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ ⇑(ConcreteCategory.hom (pullback.fst f g)) =
    ⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯))

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem setOf_isPreconnected_eq_of_ordered :
    { s : Set α | IsPreconnected s } =
      -- bounded intervals
      range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      -- unbounded intervals and `univ`
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Proof state:
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
⊢ range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}) ⊆
    {s | IsPreconnected s}

Tactic:
simp only [subset_def, forall_mem_range, uncurry, or_imp, forall_and, mem_union,
  mem_setOf_eq, insert_eq, mem_singleton_iff, forall_eq, forall_true_iff, and_true,
  isPreconnected_Icc, isPreconnected_Ico, isPreconnected_Ioc, isPreconnected_Ioo,
  isPreconnected_Ioi, isPreconnected_Iio, isPreconnected_Ici, isPreconnected_Iic,
  isPreconnected_univ, isPreconnected_empty]

Result:
no goals

Proof state:
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
⊢ {s | IsPreconnected s} =
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
refine Subset.antisymm setOf_isPreconnected_subset_of_ordered ?_

Result:
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
⊢ range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}) ⊆
    {s | IsPreconnected s}
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t ∈ ∂⁺^k 𝒜` iff `t` is exactly `k` elements less than something in `𝒜`.

See also `Finset.mem_upShadow_iterate_iff_exists_sdiff`. -/
lemma mem_upShadow_iterate_iff_exists_mem_card_add :
    t ∈ ∂⁺^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + k

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = k ↔ #t✝ = #t + k

Tactic:
rw [card_sdiff hst, tsub_eq_iff_eq_add_of_le, add_comm]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝

Tactic:
exact card_mono hst

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + k

Tactic:
refine mem_upShadow_iterate_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
  and_congr_right fun hst ↦ ?_

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = k ↔ #t✝ = #t + k
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sub_ne_zero_iff_lt {a b : Ordinal} : a - b ≠ 0 ↔ b < a

Proof state:
a b : Ordinal.{u_4}
⊢ a - b ≠ 0 ↔ b < a

Tactic:
simpa using Ordinal.sub_eq_zero_iff_le.not

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_mul_setLaverage (f : α → ℝ≥0∞) (h : μ s ≠ ∞) :
    μ s * ⨍⁻ x in s, f x ∂μ = ∫⁻ x in s, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
h : μ s ≠ ⊤
⊢ μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
have := Fact.mk h.lt_top

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
h : μ s ≠ ⊤
this : Fact (μ s < ⊤)
⊢ μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
h : μ s ≠ ⊤
this : Fact (μ s < ⊤)
⊢ μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← measure_mul_laverage, restrict_apply_univ]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_sub_le {x y g} (hx : v x ≤ g) (hy : v y ≤ g) : v (x - y) ≤ g

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : v x ≤ g
hy : v y ≤ g
⊢ v (x - y) ≤ g

Tactic:
rw [sub_eq_add_neg]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : v x ≤ g
hy : v y ≤ g
⊢ v (x + -y) ≤ g

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : v x ≤ g
hy : v y ≤ g
⊢ v (x + -y) ≤ g

Tactic:
exact v.map_add_le hx (le_trans (le_of_eq (v.map_neg y)) hy)

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem pow_equiv_pow {f1 f2 : CauSeq β abv} (hf : f1 ≈ f2) (n : ℕ) : f1 ^ n ≈ f2 ^ n

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
⊢ f1 ^ n ≈ f2 ^ n

Tactic:
induction n with
| zero => simp only [pow_zero, Setoid.refl]
| succ n ih => simpa only [pow_succ'] using mul_equiv_mul hf ih

Result:
no goals

Proof state:
case zero
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
⊢ f1 ^ 0 ≈ f2 ^ 0

Tactic:
simp only [pow_zero, Setoid.refl]

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
ih : f1 ^ n ≈ f2 ^ n
⊢ f1 ^ (n + 1) ≈ f2 ^ (n + 1)

Tactic:
simpa only [pow_succ'] using mul_equiv_mul hf ih

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem submatrix_diagonal [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l → m)
    (he : Function.Injective e) : (diagonal d).submatrix e e = diagonal (d ∘ e) :=
  ext fun i j => by
    rw [submatrix_apply]
    by_cases h : i = j
    · rw [h, diagonal_apply_eq, diagonal_apply_eq]
      simp only [Function.comp_apply] -- Porting note: (simp) added this
    · rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]

Proof state:
case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = (d ∘ e) j

Tactic:
simp only [Function.comp_apply]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ (diagonal d).submatrix e e i j = diagonal (d ∘ e) i j

Tactic:
rw [submatrix_apply]

Result:
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Proof state:
case neg
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]

Result:
no goals

Proof state:
case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
rw [h, diagonal_apply_eq, diagonal_apply_eq]

Result:
case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = (d ∘ e) j

Proof state:
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
by_cases h : i = j

Result:
case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

case neg
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j