harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem sInf_eq_boundedBy_sInfGen (m : Set (OuterMeasure α)) :
    sInf m = OuterMeasure.boundedBy (sInfGen m)

Proof state:
case refine_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)

Tactic:
refine le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => ?_

Result:
case refine_1
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (sInf m) s ≤ μ s

Proof state:
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m = boundedBy (sInfGen m)

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)

case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m

Proof state:
case refine_2
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
t : Set α
⊢ (boundedBy (sInfGen m)) t ≤ μ t

Tactic:
exact le_trans (boundedBy_le t) (iInf₂_le μ hμ)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m

Tactic:
refine le_sInf ?_

Result:
case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ ∀ b ∈ m, boundedBy (sInfGen m) ≤ b

Proof state:
case refine_1
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (sInf m) s ≤ μ s

Tactic:
apply sInf_le hμ

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ ∀ b ∈ m, boundedBy (sInfGen m) ≤ b

Tactic:
intro μ hμ t

Result:
case refine_2
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
t : Set α
⊢ (boundedBy (sInfGen m)) t ≤ μ t
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma toRange_app_val {i : Cᵒᵖ} (x : F'.obj i) :
    ((toRange p).app i x).val = p.app i x

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F'.obj i
⊢ ↑((toRange p).app i x) = p.app i x

Tactic:
simp [toRange]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Even.neg_zpow : Even n → ∀ a : α, (-a) ^ n = a ^ n

Proof state:
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
rintro ⟨c, rfl⟩ a

Result:
case intro
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)

Proof state:
case intro
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)

Tactic:
simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
lemma leadingCoeff_toLex : p.leadingCoeff toLex = p.coeff (ofLex <| p.supDegree toLex)

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ leadingCoeff (⇑toLex) p = coeff (ofLex (supDegree (⇑toLex) p)) p

Tactic:
rw [leadingCoeff]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ p (invFun (⇑toLex) (supDegree (⇑toLex) p)) = coeff (ofLex (supDegree (⇑toLex) p)) p

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ invFun (⇑toLex) (supDegree (⇑toLex) p) = ofLex (supDegree (⇑toLex) p)

Tactic:
apply toLex.injective

Result:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ toLex (invFun (⇑toLex) (supDegree (⇑toLex) p)) = toLex (ofLex (supDegree (⇑toLex) p))

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ p (invFun (⇑toLex) (supDegree (⇑toLex) p)) = coeff (ofLex (supDegree (⇑toLex) p)) p

Tactic:
apply congr_arg p.coeff

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ invFun (⇑toLex) (supDegree (⇑toLex) p) = ofLex (supDegree (⇑toLex) p)

Proof state:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ toLex (invFun (⇑toLex) (supDegree (⇑toLex) p)) = toLex (ofLex (supDegree (⇑toLex) p))

Tactic:
rw [Function.rightInverse_invFun toLex.surjective, toLex_ofLex]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_filter_iff {p : α → Bool} :
    L₁ ++ L₂ = filter p l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Proof state:
α : Type u_1
L₁ L₂ l : List α
p : α → Bool
⊢ L₁ ++ L₂ = filter p l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Tactic:
rw [eq_comm, filter_eq_append_iff]

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem rank_commutator_le_card [Finite (commutatorSet G)] :
    Group.rank (commutator G) ≤ Nat.card (commutatorSet G)

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(commutator G) ≤ Nat.card ↑(commutatorSet G)

Tactic:
rw [Subgroup.rank_congr (commutator_eq_closure G)]

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(Subgroup.closure (commutatorSet G)) ≤ Nat.card ↑(commutatorSet G)

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(Subgroup.closure (commutatorSet G)) ≤ Nat.card ↑(commutatorSet G)

Tactic:
apply Subgroup.rank_closure_finite_le_nat_card

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem ConvexOn.secant_mono_aux3 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
    (hxy : x < y) (hyz : y < z) : (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) * (z - y) ≤ (f z - f y) * (z - x)

Tactic:
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

Tactic:
have hyz' : 0 < z - y := by linarith

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

Tactic:
rw [div_le_div_iff₀ hxz' hyz']

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) * (z - y) ≤ (f z - f y) * (z - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < z - y

Tactic:
linarith

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ 0 < z - x

Tactic:
linarith

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

Tactic:
have hxz' : 0 < z - x := by linarith

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_mul_eq_mul_orderOf_of_coprime (h : Commute x y)
    (hco : (orderOf x).Coprime (orderOf y)) : orderOf (x * y) = orderOf x * orderOf y

Proof state:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ orderOf (x * y) = orderOf x * orderOf y

Tactic:
rw [orderOf, ← comp_mul_left]

Result:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 = orderOf x * orderOf y

Proof state:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 = orderOf x * orderOf y

Tactic:
exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lsub_le_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a} :
    lsub.{_, v} f ≤ a ↔ ∀ i, f i < a

Proof state:
case h.e'_2.h.a
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max v u}
a✝ : ι
⊢ f a✝ < a ↔ (succ ∘ f) a✝ ≤ a

Tactic:
simp only [comp_apply, succ_le_iff]

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max v u}
⊢ lsub f ≤ a ↔ ∀ (i : ι), f i < a

Tactic:
convert sup_le_iff.{_, v} (f := succ ∘ f) (a := a) using 2

Result:
case h.e'_2.h.a
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max v u}
a✝ : ι
⊢ f a✝ < a ↔ (succ ∘ f) a✝ ≤ a
-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_isDescendingCentralSeries :
    IsDescendingCentralSeries (lowerCentralSeries G)

Proof state:
G : Type u_1
inst✝ : Group G
⊢ IsDescendingCentralSeries (lowerCentralSeries G)

Tactic:
constructor

Result:
case left
G : Type u_1
inst✝ : Group G
⊢ lowerCentralSeries G 0 = ⊤

case right
G : Type u_1
inst✝ : Group G
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)

Proof state:
case right
G : Type u_1
inst✝ : Group G
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)

Tactic:
intro x n hxn g

Result:
case right
G : Type u_1
inst✝ : Group G
x : G
n : ℕ
hxn : x ∈ lowerCentralSeries G n
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)

Proof state:
case left
G : Type u_1
inst✝ : Group G
⊢ lowerCentralSeries G 0 = ⊤

Tactic:
rfl

Result:
no goals

Proof state:
case right
G : Type u_1
inst✝ : Group G
x : G
n : ℕ
hxn : x ∈ lowerCentralSeries G n
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)

Tactic:
exact commutator_mem_commutator hxn (mem_top g)

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis.isBasis_of_isBasis_of_subset_of_subset (hI : M.IsBasis I X) (hJ : M.IsBasis J Y)
    (hJX : J ⊆ X) (hIY : I ⊆ Y) : M.IsBasis I Y

Proof state:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
⊢ M.IsBasis I Y

Tactic:
have hI' := hI.isBasis_subset (subset_inter hI.subset hIY) inter_subset_left

Result:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
⊢ M.IsBasis I Y

Proof state:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
hJ' : M.IsBasis J (X ∩ Y)
⊢ M.IsBasis I Y

Tactic:
exact hI'.transfer hJ' inter_subset_right hJ

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
⊢ M.IsBasis I Y

Tactic:
have hJ' := hJ.isBasis_subset (subset_inter hJX hJ.subset) inter_subset_right

Result:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
hJ' : M.IsBasis J (X ∩ Y)
⊢ M.IsBasis I Y
-- Mathlib/Data/Finset/Card.lean
theorem strongDownwardInduction_eq {p : Finset α → Sort*}
    (H : ∀ t₁, (∀ {t₂ : Finset α}, #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁)
    (s : Finset α) :
    strongDownwardInduction H s = H s fun {t} ht _ => strongDownwardInduction H t ht

Proof state:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
⊢ strongDownwardInduction H s = H s fun {t} ht x => strongDownwardInduction H t ht

Tactic:
rw [strongDownwardInduction]

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem finInsepDegree_bot' :
    finInsepDegree F (⊥ : IntermediateField E K) = finInsepDegree F E

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
⊢ finInsepDegree F ↥⊥ = finInsepDegree F E

Tactic:
simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat (lift_insepDegree_bot' F E K)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma lift_eq_ofENat {x : Cardinal.{v}} {m : ℕ∞} : lift.{u} x = m ↔ x = m

Proof state:
x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x = ↑m ↔ x = ↑m

Tactic:
rw [← lift_ofENat.{u, v}, lift_inj]

Result:
no goals
-- Mathlib/Algebra/Lie/Free.lean
theorem lift_comp_of (F : FreeLieAlgebra R X →ₗ⁅R⁆ L) : lift R (F ∘ of R) = F

Proof state:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R) ((lift R).symm F) = F

Tactic:
exact (lift R).apply_symm_apply F

Result:
no goals

Proof state:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R) (⇑F ∘ of R) = F

Tactic:
rw [← lift_symm_apply]

Result:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R) ((lift R).symm F) = F
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.affine_image (f : E →ᵃ[𝕜] F) (hs : Convex 𝕜 s) : Convex 𝕜 (f '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
⊢ Convex 𝕜 (⇑f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex 𝕜 (f x) (⇑f '' s)

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex 𝕜 (f x) (⇑f '' s)

Tactic:
exact (hs hx).affine_image _

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem iSupLift_mk {i : ι} (x : K i) (hx : (x : A) ∈ T) :
    iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

Tactic:
subst hT

Result:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : ↑x ∈ iSup K
⊢ (iSupLift K dir f hf (iSup K) ⋯) ⟨↑x, hx⟩ = (f i) x

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : ↑x ∈ iSup K
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, hx⟩ = (f i) x

Tactic:
apply Set.iUnionLift_mk

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : ↑x ∈ iSup K
⊢ (iSupLift K dir f hf (iSup K) ⋯) ⟨↑x, hx⟩ = (f i) x

Tactic:
dsimp [iSupLift]

Result:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : ↑x ∈ iSup K
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, hx⟩ = (f i) x
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_mul [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α]
    (M : o → Matrix m n α) (N : o → Matrix n p α) :
    (blockDiagonal fun k => M k * N k) = blockDiagonal M * blockDiagonal N

Proof state:
case a.mk.mk
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ (if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0) =
    ∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
⊢ (blockDiagonal fun k => M k * N k) = blockDiagonal M * blockDiagonal N

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩

Result:
case a.mk.mk
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ blockDiagonal (fun k => M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')

Proof state:
case a.mk.mk
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ blockDiagonal (fun k => M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')

Tactic:
simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product]

Result:
case a.mk.mk
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ (if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0) =
    ∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem isUnit_iff_mulLeft_bijective {a : M} :
    IsUnit a ↔ Function.Bijective (a * ·) :=
  ⟨fun h ↦ ⟨h.mul_right_injective, fun y ↦ ⟨h.unit⁻¹ * y, by simp [← mul_assoc]⟩⟩, fun h ↦
    ⟨⟨a, _, (h.2 1).choose_spec, h.1
      (by simpa [mul_assoc] using congr_arg (· * a) (h.2 1).choose_spec)⟩, rfl⟩⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun x => a * x) (↑h.unit⁻¹ * y) = y

Tactic:
simp [← mul_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasSubgroupToLpTrim_left_inv (hm : m ≤ m0) :
    Function.LeftInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm)

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f) = f

Tactic:
ext1

Result:
case a
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) = ↑f

Proof state:
case a.h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) =ᶠ[ae μ] ↑↑↑f

Tactic:
exact (lpTrimToLpMeasSubgroup_ae_eq hm _).trans (lpMeasSubgroupToLpTrim_ae_eq hm _)

Result:
no goals

Proof state:
case a
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) = ↑f

Tactic:
ext1

Result:
case a.h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) =ᶠ[ae μ] ↑↑↑f

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ Function.LeftInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm)

Tactic:
intro f

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f) = f
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem abs_abv_sub_le_abv_sub (a b : R) : abs (abv a - abv b) ≤ abv (a - b) :=
  abs_sub_le_iff.2 ⟨abv.le_sub _ _, by rw [abv.map_sub]; apply abv.le_sub⟩

Proof state:
R : Type u_5
S : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ abv b - abv a ≤ abv (b - a)

Tactic:
apply abv.le_sub

Result:
no goals

Proof state:
R : Type u_5
S : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ abv b - abv a ≤ abv (a - b)

Tactic:
rw [abv.map_sub]

Result:
R : Type u_5
S : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ abv b - abv a ≤ abv (b - a)
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_le_iff : b ♯ c ≤ a ↔ (∀ b' < b, b' ♯ c < a) ∧ ∀ c' < c, b ♯ c' < a

Proof state:
a b c : Ordinal.{u}
⊢ b ♯ c ≤ a ↔ (∀ b' < b, b' ♯ c < a) ∧ ∀ c' < c, b ♯ c' < a

Tactic:
rw [← not_lt, lt_nadd_iff]

Result:
a b c : Ordinal.{u}
⊢ ¬((∃ b' < b, a ≤ b' ♯ c) ∨ ∃ c' < c, a ≤ b ♯ c') ↔ (∀ b' < b, b' ♯ c < a) ∧ ∀ c' < c, b ♯ c' < a

Proof state:
a b c : Ordinal.{u}
⊢ ¬((∃ b' < b, a ≤ b' ♯ c) ∨ ∃ c' < c, a ≤ b ♯ c') ↔ (∀ b' < b, b' ♯ c < a) ∧ ∀ c' < c, b ♯ c' < a

Tactic:
simp

Result:
no goals