harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem exists_affineBasis_of_finiteDimensional [Fintype ι] [FiniteDimensional k V]
    (h : Fintype.card ι = Module.finrank k V + 1) : Nonempty (AffineBasis ι k P)

Proof state:
case intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Set P
b : AffineBasis (↑s) k P
hb : ⇑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)

Tactic:
lift s to Finset P using b.finite_set

Result:
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ⇑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)

Proof state:
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ⇑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)

Tactic:
refine ⟨b.reindex <| Fintype.equivOfCardEq ?_⟩

Result:
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ⇑b = Subtype.val
⊢ Fintype.card ↑↑s = Fintype.card ι

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
⊢ Nonempty (AffineBasis ι k P)

Tactic:
obtain ⟨s, b, hb⟩ := AffineBasis.exists_affineBasis k V P

Result:
case intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Set P
b : AffineBasis (↑s) k P
hb : ⇑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)

Proof state:
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ⇑b = Subtype.val
⊢ Fintype.card ↑↑s = Fintype.card ι

Tactic:
rw [h, ← b.card_eq_finrank_add_one]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem norm_mem_spanNorm [Module.Free R S] {I : Ideal S} (x : S) (hx : x ∈ I) :
    Algebra.norm R x ∈ I.spanNorm R

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝ : Module.Free R S
I : Ideal S
x : S
hx : x ∈ I
⊢ (Algebra.norm R) x ∈ spanNorm R I

Tactic:
refine subset_span ⟨x, hx, ?_⟩

Result:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝ : Module.Free R S
I : Ideal S
x : S
hx : x ∈ I
⊢ (Algebra.intNorm R S) x = (Algebra.norm R) x

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝ : Module.Free R S
I : Ideal S
x : S
hx : x ∈ I
⊢ (Algebra.intNorm R S) x = (Algebra.norm R) x

Tactic:
rw [Algebra.intNorm_eq_norm]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
@[fun_prop]
lemma unitInterval.toNNReal_continuous : Continuous toNNReal

Proof state:
⊢ Continuous toNNReal

Tactic:
delta toNNReal

Result:
⊢ Continuous fun i => ⟨↑i, ⋯⟩

Proof state:
⊢ Continuous fun i => ⟨↑i, ⋯⟩

Tactic:
fun_prop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_assoc (x y z : BitVec w) : x * y * z = x * (y * z)

Proof state:
case a
w : Nat
x y z : BitVec w
⊢ (x * y * z).toFin = (x * (y * z)).toFin

Tactic:
simpa using Fin.mul_assoc ..

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
⊢ x * y * z = x * (y * z)

Tactic:
apply eq_of_toFin_eq

Result:
case a
w : Nat
x y z : BitVec w
⊢ (x * y * z).toFin = (x * (y * z)).toFin
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_eta (p : MvPolynomial σ R) : eval₂ C X p = p

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ eval₂ C X p = p

Tactic:
apply MvPolynomial.induction_on p <;>
  simp +contextual [eval₂_add, eval₂_mul]

Result:
no goals
-- Mathlib/Algebra/Module/PointwisePi.lean
theorem smul_univ_pi [∀ i, SMul K (R i)] (r : K) (t : ∀ i, Set (R i)) :
    r • pi (univ : Set ι) t = pi (univ : Set ι) (r • t) :=
  (Subset.antisymm (smul_pi_subset _ _ _)) fun x h ↦ by
    refine ⟨fun i ↦ Classical.choose (h i <| Set.mem_univ _), fun i _ ↦ ?_, funext fun i ↦ ?_⟩
    · exact (Classical.choose_spec (h i <| Set.mem_univ i)).left
    · exact (Classical.choose_spec (h i <| Set.mem_univ i)).right

Proof state:
case refine_2
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ univ.pi (r • t)
i : ι
⊢ (fun x => r • x) (fun i => Classical.choose ⋯) i = x i

Tactic:
exact (Classical.choose_spec (h i <| Set.mem_univ i)).right

Result:
no goals

Proof state:
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ univ.pi (r • t)
⊢ x ∈ r • univ.pi t

Tactic:
refine ⟨fun i ↦ Classical.choose (h i <| Set.mem_univ _), fun i _ ↦ ?_, funext fun i ↦ ?_⟩

Result:
case refine_1
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ univ.pi (r • t)
i : ι
x✝ : i ∈ univ
⊢ (fun i => Classical.choose ⋯) i ∈ t i

case refine_2
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ univ.pi (r • t)
i : ι
⊢ (fun x => r • x) (fun i => Classical.choose ⋯) i = x i

Proof state:
case refine_1
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ univ.pi (r • t)
i : ι
x✝ : i ∈ univ
⊢ (fun i => Classical.choose ⋯) i ∈ t i

Tactic:
exact (Classical.choose_spec (h i <| Set.mem_univ i)).left

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean
theorem card_algHom_le_finrank : Nat.card (M →ₐ[K] L) ≤ finrank K M

Proof state:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ Module.rank K M < ℵ₀

Tactic:
have := Module.nontrivial K L

Result:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ Module.rank K M < ℵ₀

Proof state:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ Nat.card (M →ₐ[K] L) ≤ finrank K M

Tactic:
convert toNat_le_toNat (cardinalMk_algHom_le_rank K M L) ?_

Result:
case h.e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ finrank K M = toNat (lift.{v, u_2} (Module.rank K M))

K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) < ℵ₀

Proof state:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) < ℵ₀

Tactic:
rw [lift_lt_aleph0]

Result:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ Module.rank K M < ℵ₀

Proof state:
case h.e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ finrank K M = toNat (lift.{v, u_2} (Module.rank K M))

Tactic:
rw [toNat_lift, finrank]

Result:
no goals

Proof state:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ Module.rank K M < ℵ₀

Tactic:
apply Module.rank_lt_aleph0

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic.monic (n : ℕ) (R : Type*) [Ring R] : (cyclotomic n R).Monic

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ (cyclotomic n R).Monic

Tactic:
rw [← map_cyclotomic_int]

Result:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ (map (Int.castRingHom R) (cyclotomic n ℤ)).Monic

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ (map (Int.castRingHom R) (cyclotomic n ℤ)).Monic

Tactic:
exact (int_cyclotomic_spec n).2.2.map _

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem StrictConvexOn.secant_strict_mono_aux3 (hf : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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_strict_mono_aux1 hx hz hxy hyz]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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_lt_div_iff₀ hxz' hyz']

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 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)
-- Mathlib/Logic/Relation.lean
@[simp] lemma map_id_id (r : α → β → Prop) : Relation.Map r id id = r

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
r : α → β → Prop
x✝¹ : α
x✝ : β
⊢ Relation.Map r id id x✝¹ x✝ ↔ r x✝¹ x✝

Tactic:
simp [Relation.Map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Relation.Map r id id = r

Tactic:
ext

Result:
case h.h.a
α : Type u_1
β : Type u_2
r : α → β → Prop
x✝¹ : α
x✝ : β
⊢ Relation.Map r id id x✝¹ x✝ ↔ r x✝¹ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α]
    {l : List α} :
    (unitOfList l).isEmpty = l.isEmpty

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ (unitOfList l).isEmpty = l.isEmpty

Tactic:
simp_to_raw using Raw₀.Const.isEmpty_insertManyIfNewUnit_empty_list

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem neg_rotation_neg_pi_div_two (x : V) :
    -o.rotation (-π / 2 : ℝ) x = o.rotation (π / 2 : ℝ) x

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ -(o.rotation ↑(-π / 2)) x = (o.rotation ↑(π / 2)) x

Tactic:
rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Flat.lean
theorem representablyCoflat_op_iff : RepresentablyCoflat F.op ↔ RepresentablyFlat F

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsFiltered (StructuredArrow X F)ᵒᵖ

Tactic:
apply IsFiltered.of_equivalence (structuredArrowOpEquivalence _ _).symm

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ

Tactic:
apply IsCofiltered.of_equivalence (opOpEquivalence _)

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ RepresentablyCoflat F.op ↔ RepresentablyFlat F

Tactic:
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsCofiltered (StructuredArrow X F)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F.op (op X))

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsCofiltered (StructuredArrow X F)

Tactic:
suffices IsFiltered (StructuredArrow X F)ᵒᵖ from isCofiltered_of_isFiltered_op _

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsFiltered (StructuredArrow X F)ᵒᵖ

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F.op (op X))

Tactic:
suffices IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ from isFiltered_of_isCofiltered_op _

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ

Tactic:
suffices IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ from
  IsCofiltered.of_equivalence (structuredArrowOpEquivalence _ _).op

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem liouvilleWith (hx : Liouville x) (p : ℝ) : LiouvilleWith p x

Proof state:
case intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ |x - ↑m / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊

Tactic:
refine ⟨a, hne, ?_⟩

Result:
case intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ |x - ↑a / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊

Proof state:
case intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ |x - ↑a / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊

Tactic:
rwa [rpow_natCast]

Result:
no goals

Proof state:
x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < 1 / ↑x_1 ^ ↑⌈p⌉₊

Tactic:
rintro b ⟨_hb, a, hne, hlt⟩

Result:
case intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ |x - ↑m / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊

Proof state:
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith p x

Tactic:
suffices LiouvilleWith ⌈p⌉₊ x from this.mono (Nat.le_ceil p)

Result:
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x

Proof state:
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x

Tactic:
refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩

Result:
x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < 1 / ↑x_1 ^ ↑⌈p⌉₊
-- Mathlib/Data/DFinsupp/Submonoid.lean
theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp' [AddCommMonoid γ] (S : ι → AddSubmonoid γ)
    [∀ (i) (x : S i), Decidable (x ≠ 0)] (x : γ) :
    x ∈ iSup S ↔ ∃ f : Π₀ i, S i, (f.sum fun _ xi => ↑xi) = x

Proof state:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i => (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi => ↑xi) = x

Tactic:
simp_rw [sumAddHom_apply]

Result:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (f.sum fun x => ⇑(S x).subtype) = x) ↔ ∃ f, (f.sum fun x xi => ↑xi) = x

Proof state:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (f.sum fun x => ⇑(S x).subtype) = x) ↔ ∃ f, (f.sum fun x xi => ↑xi) = x

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ x ∈ iSup S ↔ ∃ f, (f.sum fun x xi => ↑xi) = x

Tactic:
rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]

Result:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i => (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi => ↑xi) = x
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_homothety_image {d : ℝ} (hd : 0 ≤ d) (x : P) {c : 𝕜} (hc : c ≠ 0)
    (s : Set P) : μH[d] (AffineMap.homothety x c '' s) = ‖c‖₊ ^ d • μH[d] s

Proof state:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[d] (⇑(IsometryEquiv.vaddConst x) '' ((fun x => c • x) '' (⇑(IsometryEquiv.vaddConst x).symm '' s))) =
    ‖c‖₊ ^ d • μH[d] s

Tactic:
rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
  IsometryEquiv.hausdorffMeasure_image]

Result:
no goals

Proof state:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(IsometryEquiv.vaddConst x) '' ((fun x => c • x) '' (⇑(IsometryEquiv.vaddConst x).symm '' s))) =
    ‖c‖₊ ^ d • μH[d] s

Tactic:
borelize E

Result:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[d] (⇑(IsometryEquiv.vaddConst x) '' ((fun x => c • x) '' (⇑(IsometryEquiv.vaddConst x).symm '' s))) =
    ‖c‖₊ ^ d • μH[d] s

Proof state:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this :
  μH[d] (⇑(IsometryEquiv.vaddConst x) '' ((fun x => c • x) '' (⇑(IsometryEquiv.vaddConst x).symm '' s))) =
    ‖c‖₊ ^ d • μH[d] s
⊢ μH[d] (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • μH[d] s

Tactic:
simpa only [Set.image_image]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Hom.lean
lemma cancel_left {g : β →*₀ γ} {f₁ f₂ : α →*₀ β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h ↦ ext fun x ↦ hg <| by rw [← comp_apply, h,
    comp_apply], fun h ↦ h ▸ rfl⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← comp_apply, h,
comp_apply]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
lemma take_inits {n} : (l.take n).inits = l.inits.take (n + 1)

Proof state:
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits = take (n + 1) l.inits

Tactic:
apply ext_getElem <;> (simp [take_take]; omega)

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ), i < n ⊓ l.length + 1 → i < (n + 1) ⊓ (l.length + 1) → i ⊓ (n ⊓ l.length) = i ⊓ l.length

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    (take n l).inits[i] = (take (n + 1) l.inits)[i]

Tactic:
simp [take_take]

Result:
case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ), i < n ⊓ l.length + 1 → i < (n + 1) ⊓ (l.length + 1) → i ⊓ (n ⊓ l.length) = i ⊓ l.length