harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findIdx?_toArray (p : α → Bool) (l : List α) :
    l.toArray.findIdx? p = l.findIdx? p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ Array.findIdx? p l.toArray = findIdx? p l

Tactic:
rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ Option.map (fun x => ↑x) (Array.findFinIdx? p l.toArray) = Option.map (fun x => ↑x) (findFinIdx? p l)

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ Option.map (fun x => ↑x) (Array.findFinIdx? p l.toArray) = Option.map (fun x => ↑x) (findFinIdx? p l)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem sub_lt_sub_of_lt_of_le {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hz : z ≠ ⊥)
    (ht : t ≠ ⊤) : x - t < y - z :=
  add_lt_add_of_lt_of_le h (neg_le_neg_iff.2 h') (by simp [ht]) (by simp [hz])

Proof state:
x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -t ≠ ⊥

Tactic:
simp [ht]

Result:
no goals

Proof state:
x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -z ≠ ⊤

Tactic:
simp [hz]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_eq_zero_of_lt {a b : Ordinal} (h : a < b) : a / b = 0

Proof state:
a b : Ordinal.{u_4}
h : a < b
⊢ a / b = 0

Tactic:
rw [← Ordinal.le_zero, div_le <| Ordinal.pos_iff_ne_zero.1 <| (Ordinal.zero_le _).trans_lt h]

Result:
a b : Ordinal.{u_4}
h : a < b
⊢ a < b * succ 0

Proof state:
a b : Ordinal.{u_4}
h : a < b
⊢ a < b * succ 0

Tactic:
simpa only [succ_zero, mul_one] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} :
    k' ∈ Const.modify m k f ↔ k' ∈ m

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
⊢ k' ∈ modify m k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_modify]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_units_inv (f : CircleDeg1Liftˣ) : τ ↑f⁻¹ = -τ f :=
  eq_neg_iff_add_eq_zero.2 <| by
    simp [← translationNumber_mul_of_commute (Commute.refl _).units_inv_left]

Proof state:
f : CircleDeg1Liftˣ
⊢ τ ↑f⁻¹ + τ ↑f = 0

Tactic:
simp [← translationNumber_mul_of_commute (Commute.refl _).units_inv_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_self (a : Int) : a - a = 0

Proof state:
a : Int
⊢ a - a = 0

Tactic:
rw [Int.sub_eq_add_neg, Int.add_right_neg]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
protected lemma divInt_le_divInt {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) :
    a /. b ≤ c /. d ↔ a * d ≤ c * b

Proof state:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d

Tactic:
simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0]

Result:
no goals

Proof state:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a /. b ≤ c /. d ↔ a * d ≤ c * b

Tactic:
rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg]

Result:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean
theorem condition_zero (t : PushoutCocone f g) : t.ι.app WalkingSpan.zero = f ≫ t.inl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
have w := t.ι.naturality WalkingSpan.Hom.fst

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w :
  (span f g).map fst ≫ t.ι.app WalkingSpan.left =
    t.ι.app WalkingSpan.zero ≫ ((Functor.const WalkingSpan).obj t.pt).map fst
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w :
  (span f g).map fst ≫ t.ι.app WalkingSpan.left =
    t.ι.app WalkingSpan.zero ≫ ((Functor.const WalkingSpan).obj t.pt).map fst
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
dsimp at w

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w : f ≫ t.inl = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w : f ≫ t.inl = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
simpa using w.symm

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedTotalDegree'_eq_bot_iff (w : σ → M) (p : MvPolynomial σ R) :
    weightedTotalDegree' w p = ⊥ ↔ p = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ (∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → False) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
exact forall_congr' fun _ => Classical.not_not

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ weightedTotalDegree' w p = ⊥ ↔ p = 0

Tactic:
simp only [weightedTotalDegree', Finset.sup_eq_bot_iff, mem_support_iff, WithBot.coe_ne_bot,
  MvPolynomial.eq_zero_iff]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ (∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → False) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_add_left (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (f : α → E) :
    setToFun μ (T + T') (hT.add hT') f = setToFun μ T hT f + setToFun μ T' hT' f

Proof state:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hf : Integrable f μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_add_left hT hT']

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hf : Integrable f μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf, add_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_left_square_iff (f : X' ⟶ X) (g : F.obj X ⟶ Y')
    (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') :
    (f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k) ↔
      (F.map f ≫ g = h ≫ k) :=
  ⟨fun w ↦ by simpa only [Equiv.symm_apply_apply]
      using homEquiv_naturality_right_square adj _ _ _ _ w,
    homEquiv_naturality_left_square adj f g h k⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k
⊢ F.map f ≫ g = h ≫ k

Tactic:
simpa only [Equiv.symm_apply_apply]
using homEquiv_naturality_right_square adj _ _ _ _ w

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Saturated.lean
theorem ker_saturated {A₁ A₂ : Type*} [AddCommGroup A₁] [AddCommGroup A₂] [NoZeroSMulDivisors ℕ A₂]
    (f : A₁ →+ A₂) : f.ker.Saturated

Proof state:
A₁ : Type u_1
A₂ : Type u_2
inst✝² : AddCommGroup A₁
inst✝¹ : AddCommGroup A₂
inst✝ : NoZeroSMulDivisors ℕ A₂
f : A₁ →+ A₂
⊢ f.ker.Saturated

Tactic:
intro n g hg

Result:
A₁ : Type u_1
A₂ : Type u_2
inst✝² : AddCommGroup A₁
inst✝¹ : AddCommGroup A₂
inst✝ : NoZeroSMulDivisors ℕ A₂
f : A₁ →+ A₂
n : ℕ
g : A₁
hg : n • g ∈ f.ker
⊢ n = 0 ∨ g ∈ f.ker

Proof state:
A₁ : Type u_1
A₂ : Type u_2
inst✝² : AddCommGroup A₁
inst✝¹ : AddCommGroup A₂
inst✝ : NoZeroSMulDivisors ℕ A₂
f : A₁ →+ A₂
n : ℕ
g : A₁
hg : n • g ∈ f.ker
⊢ n = 0 ∨ g ∈ f.ker

Tactic:
simpa only [f.mem_ker, nsmul_eq_smul, f.map_nsmul, smul_eq_zero] using hg

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_pos_of_nextCoeff_ne_zero (h : p.nextCoeff ≠ 0) : 0 < p.natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)) ≠ 0
hpz : ¬p.natDegree = 0
⊢ 0 < p.natDegree

Tactic:
apply Nat.zero_lt_of_ne_zero hpz

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)) ≠ 0
hpz : p.natDegree = 0
⊢ 0 < p.natDegree

Tactic:
simp_all only [ne_eq, zero_le, ite_true, not_true_eq_false]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.nextCoeff ≠ 0
⊢ 0 < p.natDegree

Tactic:
rw [nextCoeff] at h

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
h : (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)) ≠ 0
⊢ 0 < p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)) ≠ 0
⊢ 0 < p.natDegree

Tactic:
by_cases hpz : p.natDegree = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)) ≠ 0
hpz : p.natDegree = 0
⊢ 0 < p.natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)) ≠ 0
hpz : ¬p.natDegree = 0
⊢ 0 < p.natDegree
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_inv [Fintype m] [DecidableEq m] (A : Matrix m m α) [Invertible A] :
    A⁻¹.IsHermitian ↔ A.IsHermitian :=
  ⟨fun h => by rw [← inv_inv_of_invertible A]; exact IsHermitian.inv h, IsHermitian.inv⟩

Proof state:
α : Type u_1
m : Type u_3
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : A⁻¹.IsHermitian
⊢ A⁻¹⁻¹.IsHermitian

Tactic:
exact IsHermitian.inv h

Result:
no goals

Proof state:
α : Type u_1
m : Type u_3
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : A⁻¹.IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← inv_inv_of_invertible A]

Result:
α : Type u_1
m : Type u_3
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : A⁻¹.IsHermitian
⊢ A⁻¹⁻¹.IsHermitian
-- Mathlib/Data/Complex/Basic.lean
theorem conj_eq_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=
  ⟨fun h => ⟨z.re, ext rfl <| eq_zero_of_neg_eq (congr_arg im h)⟩, fun ⟨h, e⟩ => by
    rw [e, conj_ofReal]⟩

Proof state:
z : ℂ
x✝ : ∃ r, z = ↑r
h : ℝ
e : z = ↑h
⊢ (starRingEnd ℂ) z = z

Tactic:
rw [e, conj_ofReal]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_inv_rpow_self {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0) : (x ^ y) ^ (1 / y) = x

Proof state:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ (1 / y) = x

Tactic:
field_simp [← rpow_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_X_pow_add {n : ℕ} (H : degree p < n) : Monic (X ^ n + p) :=
  monic_of_degree_le n
    (le_trans (degree_add_le _ _) (max_le (degree_X_pow_le _) (le_of_lt H)))
    (by rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero])

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (X ^ n + p).coeff n = 1

Tactic:
rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]

Result:
no goals
-- Mathlib/Data/Finsupp/Lex.lean
theorem lex_lt_iff_of_unique [Preorder α] [LT N] [Unique α] {a b : Lex (α →₀ N)} :
    a < b ↔ ofLex a default < ofLex b default

Proof state:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : Preorder α
inst✝¹ : LT N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ a < b ↔ (ofLex a) default < (ofLex b) default

Tactic:
simp only [lex_lt_iff, Unique.exists_iff, and_iff_right_iff_imp]

Result:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : Preorder α
inst✝¹ : LT N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ (ofLex a) default < (ofLex b) default → ∀ j < default, (ofLex a) j = (ofLex b) j

Proof state:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : Preorder α
inst✝¹ : LT N
inst✝ : Unique α
a b : Lex (α →₀ N)
x✝ : (ofLex a) default < (ofLex b) default
j : α
hj : j < default
⊢ j < j

Tactic:
simpa only [Unique.uniq] using hj

Result:
no goals

Proof state:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : Preorder α
inst✝¹ : LT N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ (ofLex a) default < (ofLex b) default → ∀ j < default, (ofLex a) j = (ofLex b) j

Tactic:
refine fun _ j hj ↦ False.elim (lt_irrefl j ?_)

Result:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : Preorder α
inst✝¹ : LT N
inst✝ : Unique α
a b : Lex (α →₀ N)
x✝ : (ofLex a) default < (ofLex b) default
j : α
hj : j < default
⊢ j < j
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_balanceR {P l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
    (H :
      (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨
        ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
    All P (@balanceR α l x r) ↔ All P l ∧ P x ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ All P (l.balanceR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [balanceR_eq_balance' hl hr sl sr H, all_balance']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_blsub_le_lift {o} (f : ∀ a < o, Ordinal) :
    cof (blsub.{u, v} o f) ≤ Cardinal.lift.{v, u} o.card

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} #o.toType

Tactic:
exact cof_lsub_le_lift _

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [← mk_toType o]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} #o.toType
-- Mathlib/Topology/List.lean
theorem nhds_cons (a : α) (l : List α) : 𝓝 (a::l) = List.cons <$> 𝓝 a <*> 𝓝 l

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l

Tactic:
rw [nhds_list, List.traverse_cons _, ← nhds_list]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Free.lean
theorem liftHom₂_congr {a b : FreeBicategory B} {f g : a ⟶ b} {η θ : Hom₂ f g} (H : Rel η θ) :
    liftHom₂ F η = liftHom₂ F θ

Proof state:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
H : Rel η θ
⊢ liftHom₂ F η = liftHom₂ F θ

Tactic:
induction H <;> (dsimp [liftHom₂]; aesop_cat)

Result:
no goals

Proof state:
case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F ((Hom₂.associator f✝ (Hom.id b✝) g✝).vcomp (Hom₂.whisker_left f✝ (Hom₂.left_unitor g✝))) =
    liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.right_unitor f✝))

Tactic:
dsimp [liftHom₂]

Result:
case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ (α_ (liftHom F f✝) (𝟙 (F.obj b✝)) (liftHom F g✝)).hom ≫ liftHom F f✝ ◁ (λ_ (liftHom F g✝)).hom =
    (ρ_ (liftHom F f✝)).hom ▷ liftHom F g✝

Proof state:
case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ (α_ (liftHom F f✝) (𝟙 (F.obj b✝)) (liftHom F g✝)).hom ≫ liftHom F f✝ ◁ (λ_ (liftHom F g✝)).hom =
    (ρ_ (liftHom F f✝)).hom ▷ liftHom F g✝

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma rnDeriv_tilted_left {ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hfν : AEMeasurable f ν) :
    (μ.tilted f).rnDeriv ν
      =ᵐ[ν] fun x ↦ ENNReal.ofReal (exp (f x) / (∫ x, exp (f x) ∂μ)) * μ.rnDeriv ν x

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ⊤

Tactic:
exact ae_of_all _ (fun x ↦ by simp [g])

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
⊢ (μ.tilted f).rnDeriv ν =ᶠ[ae ν] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x

Tactic:
let g := fun x ↦ ENNReal.ofReal (exp (f x) / (∫ x, exp (f x) ∂μ))

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ (μ.tilted f).rnDeriv ν =ᶠ[ae ν] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
x : α
⊢ g x ≠ ⊤

Tactic:
simp [g]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ AEMeasurable g ν

Tactic:
exact ((measurable_exp.comp_aemeasurable hfν).div_const _).ennreal_ofReal

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ (μ.tilted f).rnDeriv ν =ᶠ[ae ν] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x

Tactic:
refine Measure.rnDeriv_withDensity_left (μ := μ) (ν := ν) (f := g) ?_ ?_

Result:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ AEMeasurable g ν

case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ⊤
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem perfectClosure.comap_eq_of_algHom (i : E →ₐ[F] K) :
    (perfectClosure F K).comap i = perfectClosure 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
i : E →ₐ[F] K
⊢ comap i (perfectClosure F K) = perfectClosure F E

Tactic:
ext x

Result:
case h
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
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (perfectClosure F K) ↔ x ∈ perfectClosure F E

Proof state:
case h
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
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (perfectClosure F K) ↔ x ∈ perfectClosure F E

Tactic:
exact map_mem_perfectClosure_iff i

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem lexOrder_le_of_coeff_ne_zero {φ : MvPowerSeries σ R} {d : σ →₀ ℕ}
    (h : coeff R d φ ≠ 0) : lexOrder φ ≤ toLex d

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) φ ≠ 0
h' : ↑(toLex d) < φ.lexOrder
⊢ False

Tactic:
exact h (coeff_eq_zero_of_lt_lexOrder h')

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) φ ≠ 0
⊢ ¬↑(toLex d) < φ.lexOrder

Tactic:
intro h'

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) φ ≠ 0
h' : ↑(toLex d) < φ.lexOrder
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) φ ≠ 0
⊢ φ.lexOrder ≤ ↑(toLex d)

Tactic:
rw [← not_lt]

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) φ ≠ 0
⊢ ¬↑(toLex d) < φ.lexOrder
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldl_reverse {α β : Type _} {t : RBNode α} {f : β → α → β} {init : β} :
    t.reverse.foldl f init = t.foldr (flip f) init

Proof state:
α : Type u_1
β : Type u_2
t : RBNode α
f : β → α → β
init : β
⊢ foldl f init t.reverse = foldr (flip f) t init

Tactic:
simp (config := {unfoldPartialApp := true})
  [foldr_eq_foldr_toList, foldl_eq_foldl_toList, flip]

Result:
no goals
-- Mathlib/Algebra/Order/Quantale.lean
theorem mul_sup_distrib : x * (y ⊔ z) = (x * y) ⊔ (x * z)

Proof state:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ x * (y ⊔ z) = x * y ⊔ x * z

Tactic:
rw [← iSup_pair, ← sSup_pair, mul_sSup_distrib]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem leftMulMatrix_injective : Function.Injective (leftMulMatrix b) := fun x x' h ↦
  calc
    x = Algebra.lmul R S x 1 := (mul_one x).symm
    _ = Algebra.lmul R S x' 1

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x x' : S
h : (leftMulMatrix b) x = (leftMulMatrix b) x'
⊢ ((lmul R S) x) 1 = ((lmul R S) x') 1

Tactic:
rw [(LinearMap.toMatrix b b).injective h]

Result:
no goals