harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ZMod/QuotientGroup.lean
@[to_additive (attr := simp)]
lemma finite_zpowers : (zpowers a : Set α).Finite ↔ IsOfFinOrder a

Proof state:
α : Type u_3
inst✝ : Group α
a : α
⊢ (↑(zpowers a)).Finite ↔ IsOfFinOrder a

Tactic:
simp only [← orderOf_pos_iff, ← Nat.card_zpowers, Nat.card_pos_iff, ← SetLike.coe_sort_coe,
  nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, Subgroup.coe_nonempty, true_and]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_of_isCharTwoJEqZeroNF : W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) ≠ 0
⊢ (-48 * W.a₄) ^ 3 * (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) = 110592 * W.a₄ ^ 3 * -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
have h := W.Δ'.ne_zero

Result:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : ↑W.Δ' ≠ 0
⊢ W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) ≠ 0
⊢ W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
  c₄_of_isCharTwoJEqZeroNF, Δ_of_isCharTwoJEqZeroNF, div_eq_div_iff h (neg_ne_zero.1 h)]

Result:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) ≠ 0
⊢ (-48 * W.a₄) ^ 3 * (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) = 110592 * W.a₄ ^ 3 * -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : ↑W.Δ' ≠ 0
⊢ W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
rw [coe_Δ', Δ_of_isCharTwoJEqZeroNF] at h

Result:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) ≠ 0
⊢ W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem bddAbove_l_image {s : Set α} : BddAbove (l '' s) ↔ BddAbove s :=
  ⟨fun ⟨x, hx⟩ => ⟨u x, by rwa [gc.upperBounds_l_image] at hx⟩, gc.monotone_l.map_bddAbove⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
x✝ : BddAbove (l '' s)
x : β
hx : x ∈ upperBounds (l '' s)
⊢ u x ∈ upperBounds s

Tactic:
rwa [gc.upperBounds_l_image] at hx

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRank_eq_iSup_cardinalMk_indep : M.cRank = ⨆ I : {I // M.Indep I}, #I :=
  (ciSup_le' fun B ↦ le_ciSup_of_le (bddAbove_range _) ⟨B, B.2.indep⟩ <| by rfl).antisymm <|
    ciSup_le' fun I ↦
      have ⟨B, isBase, hIB⟩ := I.2.exists_isBase_superset
      le_ciSup_of_le (bddAbove_range _) ⟨B, isBase⟩ (mk_le_mk_of_subset hIB)

Proof state:
α : Type u
M : Matroid α
B : { B // M.IsBase B }
⊢ #↑↑B ≤ #↑↑⟨↑B, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
@[simp] lemma valuation_p : valuation (p : ℤ_[p]) = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p).valuation = 1

Tactic:
simp [valuation]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe :
    TendstoLocallyUniformlyOn F f p s ↔
      TendstoLocallyUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p

Tactic:
simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
  tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ (∀ (x : { a // a ∈ s }), Tendsto ((fun y => (f y.2, F y.1 y.2)) ∘ Prod.map id Subtype.val) (p ×ˢ 𝓝 x) (𝓤 β)) ↔
    ∀ (x : ↑s), Tendsto (fun y => ((f ∘ Subtype.val) y.2, F y.1 ↑y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ (∀ (x : { a // a ∈ s }), Tendsto ((fun y => (f y.2, F y.1 y.2)) ∘ Prod.map id Subtype.val) (p ×ˢ 𝓝 x) (𝓤 β)) ↔
    ∀ (x : ↑s), Tendsto (fun y => ((f ∘ Subtype.val) y.2, F y.1 ↑y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem unzip_snd : (unzip l).snd = l.map Prod.snd

Proof state:
α✝ : Type u_1
β✝ : Type u_2
n✝ : Nat
l : Vector (α✝ × β✝) n✝
⊢ l.unzip.snd = map Prod.snd l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_subset_Ici_self : Icc a b ⊆ Ici a

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Ici_self

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem restrict_toMeasurable_of_sFinite [SFinite μ] (s : Set α) :
    μ.restrict (toMeasurable μ s) = μ.restrict s :=
  ext fun t ht => by
    rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
      restrict_apply ht, inter_comm t]

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t

Tactic:
rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
  restrict_apply ht, inter_comm t]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem outerMeasure_lt_top_of_isCompact [WeaklyLocallyCompactSpace G]
    {K : Set G} (hK : IsCompact K) :
    μ.outerMeasure K < ∞

Proof state:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
inst✝ : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ μ.outerMeasure K < ⊤

Tactic:
calc
  μ.outerMeasure K ≤ μ.outerMeasure (interior F) := measure_mono h2F
  _ ≤ μ ⟨F, h1F⟩ := by
    apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset
  _ < ⊤ := μ.lt_top _

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
inst✝ : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ μ.outerMeasure (interior F) ≤ μ { carrier := F, isCompact' := h1F }

Tactic:
apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
inst✝ : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
⊢ μ.outerMeasure K < ⊤

Tactic:
rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩

Result:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
inst✝ : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ μ.outerMeasure K < ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
    (H : ∀ (a : α), a ∈ xs.reverse → P a) :
    xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse

Proof state:
α : Type ?u.128129
β : Type ?u.128170
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs.reverse → P a
a : α
h : a ∈ xs
⊢ a ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs.reverse → P a
⊢ pmap f xs.reverse H = (pmap f xs ⋯).reverse

Tactic:
induction xs <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_natCast [NatPowAssoc R] (n k : ℕ) : choose (n : R) k = Nat.choose n k

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n k : ℕ
⊢ choose (↑n) k = ↑(n.choose k)

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
  ← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ← Nat.cast_mul,
  ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_commonNeighbors_le_degree_left [DecidableRel G.Adj] (v w : V) :
    Fintype.card (G.commonNeighbors v w) ≤ G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree v

Tactic:
rw [← card_neighborSet_eq_degree]

Result:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ Fintype.card ↑(G.neighborSet v)

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ Fintype.card ↑(G.neighborSet v)

Tactic:
exact Set.card_le_card Set.inter_subset_left

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite coproducts, then `F.unop : C ⥤ D` preserves finite
    products. -/
lemma preservesFiniteProducts_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesFiniteCoproducts F] :
    PreservesFiniteProducts F.unop where
  preserves _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_unop

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem add_lf_add_right : ∀ {b c : Game} (_ : b ⧏ c) (a), (b + a : Game) ⧏ c + a

Proof state:
⊢ ∀ {b c : Game}, b ⧏ c → ∀ (a : Game), b + a ⧏ c + a

Tactic:
rintro ⟨b⟩ ⟨c⟩ h ⟨a⟩

Result:
case mk.mk.mk
b✝ : Game
b : PGame
c✝ : Game
c : PGame
h : Quot.mk (⇑setoid) b ⧏ Quot.mk (⇑setoid) c
a✝ : Game
a : PGame
⊢ Quot.mk (⇑setoid) b + Quot.mk (⇑setoid) a ⧏ Quot.mk (⇑setoid) c + Quot.mk (⇑setoid) a

Proof state:
case mk.mk.mk
b✝ : Game
b : PGame
c✝ : Game
c : PGame
h : Quot.mk (⇑setoid) b ⧏ Quot.mk (⇑setoid) c
a✝ : Game
a : PGame
⊢ Quot.mk (⇑setoid) b + Quot.mk (⇑setoid) a ⧏ Quot.mk (⇑setoid) c + Quot.mk (⇑setoid) a

Tactic:
apply PGame.add_lf_add_right h

Result:
no goals
-- Mathlib/Analysis/Convex/Quasiconvex.lean
theorem QuasiconvexOn.convex_lt (hf : QuasiconvexOn 𝕜 s f) (r : β) :
    Convex 𝕜 ({ x ∈ s | f x < r })

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ f x < r}

Tactic:
have h := hf _ ⟨hx.1, le_max_left _ _⟩ ⟨hy.1, le_max_right _ _⟩ ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ f x ⊔ f y}
⊢ a • x + b • y ∈ {x | x ∈ s ∧ f x < r}

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ f x ⊔ f y}
⊢ a • x + b • y ∈ {x | x ∈ s ∧ f x < r}

Tactic:
exact ⟨h.1, h.2.trans_lt <| max_lt hx.2 hy.2⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ f x < r}

Tactic:
refine fun x hx y hy a b ha hb hab => ?_

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ f x < r}
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_mul_rank_top (h : A ≤ B) : relrank A B * Module.rank B E = Module.rank A E

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
this✝ : Algebra ↥A ↥B := (inclusion h).toAlgebra
this : IsScalarTower (↥A) (↥B) E
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
exact rank_mul_rank A B E

Result:
no goals

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
haveI : IsScalarTower A B E := IsScalarTower.of_algebraMap_eq' rfl

Result:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
this✝ : Algebra ↥A ↥B := (inclusion h).toAlgebra
this : IsScalarTower (↥A) (↥B) E
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
letI : Algebra A B := (inclusion h).toAlgebra

Result:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
rw [relrank_eq_rank_of_le h]

Result:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem sigmaIsoSigma_inv_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) (x : α i) :
    (sigmaIsoSigma α).inv ⟨i, x⟩ = (Sigma.ι α i :) x

Proof state:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom (sigmaIsoSigma α).inv) ⟨i, x⟩ = (ConcreteCategory.hom (Sigma.ι α i)) x

Tactic:
rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Iso.hom_inv_id,
  Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/Free.lean
theorem hom_ext {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=
  (DFunLike.ext _ _) fun x ↦ recOnMul x (congr_fun h) <| by intros; simp only [map_mul, *]

Proof state:
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)

Tactic:
simp only [map_mul, *]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x : FreeMagma α
⊢ ∀ (x y : FreeMagma α), f x = g x → f y = g y → f (x * y) = g (x * y)

Tactic:
intros

Result:
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_add_comm {n m k : Nat} (h : k ≤ n) : n + m - k = n - k + m

Proof state:
n m k : Nat
h : k ≤ n
⊢ n + m - k = n - k + m

Tactic:
rw [Nat.sub_eq_iff_eq_add (Nat.le_trans h (Nat.le_add_right ..))]

Result:
n m k : Nat
h : k ≤ n
⊢ n + m = n - k + m + k

Proof state:
n m k : Nat
h : k ≤ n
⊢ n + m = n - k + m + k

Tactic:
rwa [Nat.add_right_comm, Nat.sub_add_cancel]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : ∀ p ∈ f.support, Prime p) :
    f = n.factorization ↔ f.prod (· ^ ·) = n :=
  ⟨fun h => by rw [h, factorization_prod_pow_eq_self hn], fun h => by
    rw [← h, prod_pow_factorization_eq_self hf]⟩

Proof state:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
h : (f.prod fun x1 x2 => x1 ^ x2) = n
⊢ f = n.factorization

Tactic:
rw [← h, prod_pow_factorization_eq_self hf]

Result:
no goals

Proof state:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
h : f = n.factorization
⊢ (f.prod fun x1 x2 => x1 ^ x2) = n

Tactic:
rw [h, factorization_prod_pow_eq_self hn]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Constructions.lean
/-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
component is. -/
@[to_additive pi_norm_le_iff_of_nonneg "The seminorm of an element in a product space is `≤ r` if
and only if the norm of each component is."]
lemma pi_norm_le_iff_of_nonneg' (hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ i, ‖x i‖ ≤ r

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedGroup (π i)
x : (i : ι) → π i
r : ℝ
hr : 0 ≤ r
⊢ ‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

Tactic:
simp only [← dist_one_right, dist_pi_le_iff hr, Pi.one_apply]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem norm_toContinuousLinearMap_le (f : E →ₛₗᵢ[σ₁₂] F) : ‖f.toContinuousLinearMap‖ ≤ 1 :=
  f.toContinuousLinearMap.opNorm_le_bound zero_le_one fun x => by simp

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗᵢ[σ₁₂] F
x : E
⊢ ‖f.toContinuousLinearMap x‖ ≤ 1 * ‖x‖

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem colimitUncurryIsoColimitCompColim_ι_ι_inv {j} {k} :
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv =
      colimit.ι (uncurry.obj F) (j, k)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (F.obj j) k ≫
      colimit.ι (F ⋙ colim) j ≫
        colimit.desc (F ⋙ colim)
          (coconeOfCoconeUncurry (fun j => colimit.isColimit (F.obj j)) (colimit.cocone (uncurry.obj F))) =
    colimit.ι (uncurry.obj F) (j, k)

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv =
    colimit.ι (uncurry.obj F) (j, k)

Tactic:
dsimp [colimitUncurryIsoColimitCompColim, IsColimit.coconePointUniqueUpToIso,
  IsColimit.uniqueUpToIso]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (F.obj j) k ≫
      colimit.ι (F ⋙ colim) j ≫
        colimit.desc (F ⋙ colim)
          (coconeOfCoconeUncurry (fun j => colimit.isColimit (F.obj j)) (colimit.cocone (uncurry.obj F))) =
    colimit.ι (uncurry.obj F) (j, k)
-- Mathlib/Data/Set/Lattice.lean
theorem diff_iUnion [Nonempty ι] (s : Set β) (t : ι → Set β) : (s \ ⋃ i, t i) = ⋂ i, s \ t i

Proof state:
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ ⋂ i, s ∩ (t i)ᶜ = ⋂ i, s \ t i

Tactic:
rfl

Result:
no goals

Proof state:
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ s \ ⋃ i, t i = ⋂ i, s \ t i

Tactic:
rw [diff_eq, compl_iUnion, inter_iInter]

Result:
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ ⋂ i, s ∩ (t i)ᶜ = ⋂ i, s \ t i
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDeriv_succ_eq_comp_right {n : ℕ} :
    iteratedFDeriv 𝕜 (n + 1) f x =
      ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x

Proof state:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) (init m)) (m (last n)) =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x) m

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ iteratedFDeriv 𝕜 (n + 1) f x =
    (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x

Tactic:
ext m

Result:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDeriv 𝕜 (n + 1) f x) m =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x) m

Proof state:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDeriv 𝕜 (n + 1) f x) m =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x) m

Tactic:
rw [iteratedFDeriv_succ_apply_right]

Result:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) (init m)) (m (last n)) =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x) m
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_triangle_right (x y z : ∀ i, β i) :
    hammingDist x y ≤ hammingDist x z + hammingDist y z

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist y z

Tactic:
rw [hammingDist_comm y]

Result:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y

Tactic:
exact hammingDist_triangle _ _ _

Result:
no goals