harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem integral_condExpL2_eq (hm : m ≤ m0) (f : Lp E' 2 μ) (hs : MeasurableSet[m] s)
    (hμs : μ s ≠ ∞) : ∫ x in s, (condExpL2 E' 𝕜 hm f : α → E') x ∂μ = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (a : α) in s, (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) a ∂μ = 0

Tactic:
refine integral_eq_zero_of_forall_integral_inner_eq_zero 𝕜 _ ?_ ?_

Result:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)

case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∀ (c : E'), ∫ (x : α) in s, inner c ((↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) x) ∂μ = 0

Proof state:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Integrable (↑↑(↑((condExpL2 E' 𝕜 hm) f) - f)) (μ.restrict s)

Tactic:
exact integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem lift_mkRingHom_apply (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y) (x) :
    lift ⟨f, w⟩ (mkRingHom r x) = f x

Proof state:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ (lift ⟨f, w⟩) ((mkRingHom r) x) = f x

Tactic:
simp_rw [lift_def, preLift_def, mkRingHom_def]

Result:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ ({
          toFun := fun f =>
            { toFun := fun x => Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F =>
            ⟨F.comp
                { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x) =
    f x

Proof state:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ ({
          toFun := fun f =>
            { toFun := fun x => Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F =>
            ⟨F.comp
                { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x) =
    f x

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[simp]
lemma reindex_id : reindex id S = 𝟙 𝔸(n; S)

Proof state:
n : Type v
S : Scheme
⊢ reindex id S = 𝟙 𝔸(n; S)

Tactic:
ext1 <;> simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem le_of_forall_nnreal_lt {x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, ↑r < x → ↑r ≤ y) : x ≤ y

Proof state:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0∞
hr : r < x
⊢ r ≤ y

Tactic:
lift r to ℝ≥0 using ne_top_of_lt hr

Result:
case intro
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0
hr : ↑r < x
⊢ ↑r ≤ y

Proof state:
case intro
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0
hr : ↑r < x
⊢ ↑r ≤ y

Tactic:
exact h r hr

Result:
no goals

Proof state:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
⊢ x ≤ y

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_

Result:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0∞
hr : r < x
⊢ r ≤ y
-- Mathlib/Topology/Algebra/ContinuousAffineMap.lean
theorem to_continuousMap_injective {f g : P →ᴬ[R] Q} (h : (f : C(P, Q)) = (g : C(P, Q))) :
    f = g

Proof state:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →ᴬ[R] Q
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a

Result:
case h
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →ᴬ[R] Q
h : ↑f = ↑g
a : P
⊢ f a = g a

Proof state:
case h
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →ᴬ[R] Q
h : ↑f = ↑g
a : P
⊢ f a = g a

Tactic:
exact ContinuousMap.congr_fun h a

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem succ_to_nat : ∀ n, (succ n : ℕ) = n + 1
  | 1 => rfl
  | bit0 _ => rfl
  | bit1 p =>
    (congr_arg (fun n ↦ n + n) (succ_to_nat p)).trans <|
      show ↑p + 1 + ↑p + 1 = ↑p + ↑p + 1 + 1 by simp [add_left_comm]

Proof state:
p : PosNum
⊢ ↑p + 1 + ↑p + 1 = ↑p + ↑p + 1 + 1

Tactic:
simp [add_left_comm]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem quotient_preimage_image_eq_union_mul (U : Set α) :
    letI := orbitRel G α
    Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g : G, (g • ·) '' U

Proof state:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ g⁻¹ • a ∈ U

Tactic:
rw [← hu₂]

Result:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ g⁻¹ • (fun x => g • x) u ∈ U

Proof state:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ a ∈ f ⁻¹' (f '' U)

Tactic:
rw [Set.mem_preimage, Set.mem_image]

Result:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ ∃ x ∈ U, f x = f a

Proof state:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ g⁻¹ • (fun x => g • x) u ∈ U

Tactic:
convert hu₁

Result:
case h.e'_5
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ g⁻¹ • (fun x => g • x) u = u
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem gcd_cons_div_right : gcd (x::xs) ∣ gcd xs

Proof state:
x : Int
xs : List Int
⊢ gcd (x :: xs) ∣ gcd xs

Tactic:
simp only [gcd, List.foldr_cons]

Result:
x : Int
xs : List Int
⊢ x.natAbs.gcd (List.foldr (fun x g => x.natAbs.gcd g) 0 xs) ∣ List.foldr (fun x g => x.natAbs.gcd g) 0 xs

Proof state:
x : Int
xs : List Int
⊢ x.natAbs.gcd (List.foldr (fun x g => x.natAbs.gcd g) 0 xs) ∣ List.foldr (fun x g => x.natAbs.gcd g) 0 xs

Tactic:
apply Nat.gcd_dvd_right

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem ball_subset_univBall_target (c : P) (r : ℝ) : ball c r ⊆ (univBall c r).target

Proof state:
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (univBall c r).target

Tactic:
rw [univBall, dif_neg hr]

Result:
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph.target

Proof state:
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph.target

Tactic:
exact subset_univ _

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball c r ⊆ (univBall c r).target

Tactic:
rw [univBall_target c hr]

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ball c r ⊆ (univBall c r).target

Tactic:
by_cases hr : 0 < r

Result:
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball c r ⊆ (univBall c r).target

case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (univBall c r).target
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_union_inter (hs : s.Finite) (ht : t.Finite) :
    ((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i) = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
lift s to Finset α using hs

Result:
case intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Proof state:
case intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
lift t to Finset α using ht

Result:
case intro.intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i

Proof state:
case intro.intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i

Tactic:
classical
  rw [← Finset.coe_union, ← Finset.coe_inter]
  simp only [finprod_mem_coe_finset, Finset.prod_union_inter]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑(s ∪ t)), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑(s ∩ t)), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i

Tactic:
simp only [finprod_mem_coe_finset, Finset.prod_union_inter]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i

Tactic:
rw [← Finset.coe_union, ← Finset.coe_inter]

Result:
case intro.intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑(s ∪ t)), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑(s ∩ t)), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_sdiff (a : α) : limsup u f \ a = limsup (fun b => u b \ a) f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ

Tactic:
simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun b => u b \ a) f

Tactic:
simp only [limsup_eq_iInf_iSup, sdiff_eq]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ

Tactic:
rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma transfiniteCompositionsOfShape_eq_of_orderIso (e : J ≃o J') :
    W.transfiniteCompositionsOfShape J =
      W.transfiniteCompositionsOfShape J'

Proof state:
case h
C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
e : J ≃o J'
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ W.transfiniteCompositionsOfShape J f ↔ W.transfiniteCompositionsOfShape J' f

Tactic:
exact ⟨fun ⟨h⟩ ↦ ⟨h.ofOrderIso e.symm⟩, fun ⟨h⟩ ↦ ⟨h.ofOrderIso e⟩⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
e : J ≃o J'
⊢ W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J'

Tactic:
ext _ _ f

Result:
case h
C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
e : J ≃o J'
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ W.transfiniteCompositionsOfShape J f ↔ W.transfiniteCompositionsOfShape J' f
-- Mathlib/RingTheory/DedekindDomain/Different.lean
@[simp]
lemma dual_dual :
    dual A K (dual A K I) = I

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ dual A K (dual A K I) = I

Tactic:
rw [dual_eq_mul_inv, dual_eq_mul_inv A K (I := I), mul_inv, inv_inv, ← mul_assoc, mul_inv_cancel₀,
  one_mul]

Result:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ dual A K 1 ≠ 0

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ dual A K 1 ≠ 0

Tactic:
rw [dual_ne_zero_iff]

Result:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ 1 ≠ 0
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
lemma addRothNumber_le_ruzsaSzemerediNumber :
    card α * addRothNumber (univ : Finset α) ≤ ruzsaSzemerediNumber (Sum α (Sum α α))

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
s : Finset α
hscard : #s = addRothNumber univ
hs : ThreeAPFree ↑s
this : NoAccidental (triangleIndices s)
⊢ Fintype.card α * addRothNumber univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Tactic:
rw [← hscard, ← card_triangleIndices, ← card_triangles]

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
s : Finset α
hscard : #s = addRothNumber univ
hs : ThreeAPFree ↑s
this : NoAccidental (triangleIndices s)
⊢ #((graph (triangleIndices s)).cliqueFinset 3) ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
s : Finset α
hscard : #s = addRothNumber univ
hs : ThreeAPFree ↑s
⊢ Fintype.card α * addRothNumber univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Tactic:
haveI := noAccidental hs

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
s : Finset α
hscard : #s = addRothNumber univ
hs : ThreeAPFree ↑s
this : NoAccidental (triangleIndices s)
⊢ Fintype.card α * addRothNumber univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
s : Finset α
hscard : #s = addRothNumber univ
hs : ThreeAPFree ↑s
this : NoAccidental (triangleIndices s)
⊢ #((graph (triangleIndices s)).cliqueFinset 3) ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Tactic:
exact (locallyLinear hs).le_ruzsaSzemerediNumber

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
⊢ Fintype.card α * addRothNumber univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Tactic:
obtain ⟨s, -, hscard, hs⟩ := addRothNumber_spec (univ : Finset α)

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
s : Finset α
hscard : #s = addRothNumber univ
hs : ThreeAPFree ↑s
⊢ Fintype.card α * addRothNumber univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma minpolyDiv_spec :
    minpolyDiv R x * (X - C x) = (minpoly R x).map (algebraMap R S)

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ minpolyDiv R x * (X - C x) = map (algebraMap R S) (minpoly R x)

Tactic:
delta minpolyDiv

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ map (algebraMap R S) (minpoly R x) /ₘ (X - C x) * (X - C x) = map (algebraMap R S) (minpoly R x)

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ map (algebraMap R S) (minpoly R x) /ₘ (X - C x) * (X - C x) = map (algebraMap R S) (minpoly R x)

Tactic:
rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map, ← aeval_def, minpoly.aeval]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
/-- The absolute value satisfies the triangle inequality. -/
@[to_additive "The absolute value satisfies the triangle inequality."]
lemma mabs_mul_le (a b : α) : |a * b|ₘ ≤ |a|ₘ * |b|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs (a * b) ≤ mabs a * mabs b

Tactic:
apply sup_le

Result:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b ≤ mabs a * mabs b

case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ mabs a * mabs b

Proof state:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ mabs a * mabs b

Tactic:
rw [mul_inv]

Result:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a⁻¹ * b⁻¹ ≤ mabs a * mabs b

Proof state:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b ≤ mabs a * mabs b

Tactic:
exact mul_le_mul' (le_mabs_self a) (le_mabs_self b)

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a⁻¹ * b⁻¹ ≤ mabs a * mabs b

Tactic:
exact mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)

Result:
no goals