harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft {Y Y' Z : C} [ExactPairing Y Y']
    (f : Y' ⟶ Z) : (tensorLeftHomEquiv _ _ _ _).symm (η_ _ _ ≫ Y ◁ f) = (ρ_ _).hom ≫ f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ Y ◁ f) = (ρ_ Y').hom ≫ f

Tactic:
calc
  _ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by
    dsimp [tensorLeftHomEquiv]; monoidal
  _ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by
    rw [whisker_exchange]; monoidal
  _ = _ := by rw [coevaluation_evaluation'']; monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ Y ◁ f) = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z

Tactic:
dsimp [tensorLeftHomEquiv]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Y' ◁ (η_ Y Y' ≫ Y ◁ f) ≫ (α_ Y' Y Z).inv ≫ ε_ Y Y' ▷ Z ≫ (λ_ Z).hom =
    Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f

Tactic:
rw [whisker_exchange]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Y' ◁ η_ Y Y' ⊗≫ (ε_ Y Y' ▷ Y' ≫ 𝟙_ C ◁ f) ⊗≫ 𝟙 Z = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f = (ρ_ Y').hom ≫ f

Tactic:
rw [coevaluation_evaluation'']

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢  ⊗𝟙.hom ⊗≫ f = (ρ_ Y').hom ≫ f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢  ⊗𝟙.hom ⊗≫ f = (ρ_ Y').hom ≫ f

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Y' ◁ (η_ Y Y' ≫ Y ◁ f) ≫ (α_ Y' Y Z).inv ≫ ε_ Y Y' ▷ Z ≫ (λ_ Z).hom =
    Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Y' ◁ η_ Y Y' ⊗≫ (ε_ Y Y' ▷ Y' ≫ 𝟙_ C ◁ f) ⊗≫ 𝟙 Z = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f

Tactic:
monoidal

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
@[reassoc]
lemma whiskerLeft_curry'_ihom_ev_app {X Y : C} [Closed X] (f : X ⟶ Y) :
    X ◁ curry' f ≫ (ihom.ev X).app Y = (ρ_ _).hom ≫ f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
f : X ⟶ Y
⊢ X ◁ curry ((ρ_ X).hom ≫ f) ≫ (ihom.ev X).app Y = (ρ_ X).hom ≫ f

Tactic:
simp only [whiskerLeft_curry_ihom_ev_app]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
f : X ⟶ Y
⊢ X ◁ curry' f ≫ (ihom.ev X).app Y = (ρ_ X).hom ≫ f

Tactic:
dsimp [curry']

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
f : X ⟶ Y
⊢ X ◁ curry ((ρ_ X).hom ≫ f) ≫ (ihom.ev X).app Y = (ρ_ X).hom ≫ f
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem circulant_mul [Semiring α] [Fintype n] [AddGroup n] (v w : n → α) :
    circulant v * circulant w = circulant (circulant v *ᵥ w)

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∀ (x : n), v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)

Tactic:
intro x

Result:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)

Tactic:
simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]

Result:
no goals

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j

Tactic:
simp only [mul_apply, mulVec, circulant_apply, dotProduct]

Result:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, v (i - j - x) * w x

Proof state:
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
⊢ circulant v * circulant w = circulant (circulant v *ᵥ w)

Tactic:
ext i j

Result:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, v (i - j - x) * w x

Tactic:
refine Fintype.sum_equiv (Equiv.subRight j) _ _ ?_

Result:
case a
α : Type u_1
n : Type u_3
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∀ (x : n), v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_mono [Preorder β] (s : Set α) {f g : α →ₛ β} (H : f ≤ g) :
    f.restrict s ≤ g.restrict s :=
  if hs : MeasurableSet s then fun x => by
    simp only [coe_restrict _ hs, indicator_le_indicator (H x)]
  else by simp only [restrict_of_not_measurable hs, le_refl]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : ¬MeasurableSet s
⊢ f.restrict s ≤ g.restrict s

Tactic:
simp only [restrict_of_not_measurable hs, le_refl]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : MeasurableSet s
x : α
⊢ (f.restrict s) x ≤ (g.restrict s) x

Tactic:
simp only [coe_restrict _ hs, indicator_le_indicator (H x)]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem mk_out_eq_mul (H K : Subgroup G) (g : G) :
    ∃ h k : G, h ∈ H ∧ k ∈ K ∧ (mk H K g : Quotient ↑H ↑K).out = h * g * k

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
refine ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq ?_)⟩

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
⊢ h * (Quotient.out (mk H K g) * k) = g

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
⊢ h * (Quotient.out (mk H K g) * k) = g

Tactic:
rw [← mul_assoc, ← T]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K (Quotient.out (mk H K g)) = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
rw [out_eq'] at this

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
have := eq H K (mk H K g : Quotient ↑H ↑K).out g

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K (Quotient.out (mk H K g)) = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k
-- Mathlib/Algebra/Polynomial/Degree/Monomial.lean
lemma natDegree_le_pred (hf : p.natDegree ≤ n) (hn : p.coeff n = 0) : p.natDegree ≤ n - 1

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
aesop

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1

Tactic:
refine (Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_

Result:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
h : p.natDegree = n.succ
⊢ False

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ 0
hn : p.coeff 0 = 0
⊢ p.natDegree ≤ 0 - 1

Tactic:
exact hf

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn

Result:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ n
hn : p.coeff n = 0
⊢ p.natDegree ≤ n - 1

Tactic:
obtain _ | n := n

Result:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ 0
hn : p.coeff 0 = 0
⊢ p.natDegree ≤ 0 - 1

case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_nonneg [PosMulMono G₀] (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
  | (n : ℕ) => by rw [zpow_natCast]; exact pow_nonneg ha _
  |-(n + 1 : ℕ) => by rw [zpow_neg, inv_nonneg, zpow_natCast]; exact pow_nonneg ha _

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (-↑(n + 1))

Tactic:
rw [zpow_neg, inv_nonneg, zpow_natCast]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)

Tactic:
exact pow_nonneg ha _

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n

Tactic:
exact pow_nonneg ha _

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ ↑n

Tactic:
rw [zpow_natCast]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[simp]
lemma Scheme.iso_hom_base_inv_base_apply {X Y : Scheme.{u}} (e : X ≅ Y) (x : X) :
    (e.inv.base (e.hom.base x)) = x

Proof state:
X Y : Scheme
e : X ≅ Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (e.hom.base ≫ e.inv.base)) x = (ConcreteCategory.hom (𝟙 X.toPresheafedSpace).base) x

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
e : X ≅ Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x) = x

Tactic:
show (e.hom.base ≫ e.inv.base) x = 𝟙 X.toPresheafedSpace x

Result:
X Y : Scheme
e : X ≅ Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (e.hom.base ≫ e.inv.base)) x = (ConcreteCategory.hom (𝟙 X.toPresheafedSpace).base) x
-- Mathlib/Order/Atoms.lean
theorem isStronglyCoatomic_dual_iff_is_stronglyAtomic :
    IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

Proof state:
α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈᵒᵈ ↔ IsStronglyAtomic α

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Result:
α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈᵒᵈ ↔ IsStronglyAtomic α
-- Mathlib/Analysis/Complex/OperatorNorm.lean
theorem imCLM_norm : ‖imCLM‖ = 1 :=
  le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _) <|
    calc
      1 = ‖imCLM I‖

Proof state:
⊢ 1 = ‖imCLM I‖

Tactic:
simp

Result:
no goals

Proof state:
⊢ ‖I‖ ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SupIndep.lean
lemma iSupIndep.of_coe_Iic_comp {ι : Sort*} {a : α} {t : ι → Set.Iic a}
    (ht : iSupIndep ((↑) ∘ t : ι → α)) : iSupIndep t

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
ht : iSupIndep (Subtype.val ∘ t)
⊢ iSupIndep t

Tactic:
intro i x

Result:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
ht : iSupIndep (Subtype.val ∘ t)
i : ι
x : ↑(Iic a)
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
i : ι
x : ↑(Iic a)
ht : Disjoint ↑(t i) ↑(⨆ i_1, ⨆ (_ : i_1 ≠ i), t i_1)
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Tactic:
exact @ht x

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
ht : iSupIndep (Subtype.val ∘ t)
i : ι
x : ↑(Iic a)
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Tactic:
specialize ht i

Result:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
i : ι
x : ↑(Iic a)
ht : Disjoint ((Subtype.val ∘ t) i) (⨆ j, ⨆ (_ : j ≠ i), (Subtype.val ∘ t) j)
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
i : ι
x : ↑(Iic a)
ht : Disjoint ((Subtype.val ∘ t) i) (⨆ j, ⨆ (_ : j ≠ i), (Subtype.val ∘ t) j)
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Tactic:
simp_rw [Function.comp_apply, ← Set.Iic.coe_iSup] at ht

Result:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
i : ι
x : ↑(Iic a)
ht : Disjoint ↑(t i) ↑(⨆ i_1, ⨆ (_ : i_1 ≠ i), t i_1)
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥
-- Mathlib/Data/Set/Insert.lean
theorem ssubset_singleton_iff {s : Set α} {x : α} : s ⊂ {x} ↔ s = ∅

Proof state:
α : Type u
s : Set α
x : α
⊢ s = ∅ → s ≠ {x}

Tactic:
exact fun h => h ▸ (singleton_ne_empty _).symm

Result:
no goals

Proof state:
α : Type u
s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅

Tactic:
rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false,
  and_iff_left_iff_imp]

Result:
α : Type u
s : Set α
x : α
⊢ s = ∅ → s ≠ {x}
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem cos_oangle_eq_inner_div_norm_mul_norm {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.Angle.cos (o.oangle x y) = ⟪x, y⟫ / (‖x‖ * ‖y‖)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)

Tactic:
field_simp [norm_ne_zero_iff.2 hx, norm_ne_zero_iff.2 hy]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = inner x y / (‖x‖ * ‖y‖)

Tactic:
rw [o.inner_eq_norm_mul_norm_mul_cos_oangle]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)
-- Mathlib/Data/Finset/Card.lean
/-- Reorder a finset.

The difference with `Finset.card_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.card_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains, rather than being non-dependent functions. -/
lemma card_bij' (i : ∀ a ∈ s, β) (j : ∀ a ∈ t, α) (hi : ∀ a ha, i a ha ∈ t)
    (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) : #s = #t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
⊢ #s = #t

Tactic:
refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯

Tactic:
simp only [eq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2

Tactic:
rw [← left_inv a1 h1, ← left_inv a2 h2]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯
-- Mathlib/Data/Tree/Basic.lean
theorem left_node_right_eq_self : ∀ {x : Tree Unit} (_hx : x ≠ nil), x.left △ x.right = x
  | nil, h => by trivial
  | node _ _ _, _ => rfl

Proof state:
h : nil ≠ nil
⊢ node () nil.left nil.right = nil

Tactic:
trivial

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq_lintegral {f : α →ₛ ℝ} (hf : Integrable f μ) (h_pos : 0 ≤ᵐ[μ] f) :
    f.integral μ = ENNReal.toReal (∫⁻ a, ENNReal.ofReal (f a) ∂μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
have : f =ᵐ[μ] f.map (ENNReal.toReal ∘ ENNReal.ofReal) :=
  h_pos.mono fun a h => (ENNReal.toReal_ofReal h).symm

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)

case hg0
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ ENNReal.ofReal 0 = 0

case ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ ∀ (b : ℝ), ENNReal.ofReal b ≠ ⊤

Tactic:
exacts [integral_congr hf this, ENNReal.ofReal_zero, fun b => ENNReal.ofReal_ne_top]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
rw [← integral_eq_lintegral' hf]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)

case hg0
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ ENNReal.ofReal 0 = 0

case ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (⇑f) μ
h_pos : 0 ≤ᶠ[ae μ] ⇑f
this : ⇑f =ᶠ[ae μ] ⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ ∀ (b : ℝ), ENNReal.ofReal b ≠ ⊤
-- Mathlib/RingTheory/Ideal/Operations.lean
lemma radical_pow : ∀ {n}, n ≠ 0 → radical (I ^ n) = radical I
  | 1, _ => by simp
  | n + 2, _ => by rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
x✝ : 1 ≠ 0
⊢ (I ^ 1).radical = I.radical

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (I ^ (n + 2)).radical = I.radical

Tactic:
rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem IsPreconnected.subset_isClopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t)
    (hne : (s ∩ t).Nonempty) : s ⊆ t :=
  hs.subset_left_of_subset_union ht.isOpen ht.compl.isOpen disjoint_compl_right (by simp) hne

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsClopen t
hne : (s ∩ t).Nonempty
⊢ s ⊆ t ∪ tᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
lemma iSup_coe_eapprox (hf : Measurable f) : ⨆ n, ⇑(eapprox f n) = f

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ⇑(eapprox f n) = f

Tactic:
simpa [funext_iff] using iSup_eapprox_apply hf

Result:
no goals