harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NAry.lean
theorem image_image₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
    (image₂ f s t).image g = image₂ f' (s.image g₁) (t.image g₂) :=
  coe_injective <| by
    push_cast
    exact image_image2_distrib h_distrib

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g₁ s) (image g₂ t))

Tactic:
push_cast

Result:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f ↑s ↑t = image2 f' (g₁ '' ↑s) (g₂ '' ↑t)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f ↑s ↑t = image2 f' (g₁ '' ↑s) (g₂ '' ↑t)

Tactic:
exact image_image2_distrib h_distrib

Result:
no goals
-- Mathlib/Data/NNRat/BigOperators.lean
theorem toNNRat_prod_of_nonneg {s : Finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) :
    (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat

Proof state:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat

Tactic:
rw [← coe_inj, coe_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]

Result:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∏ i ∈ s, f i = ∏ a ∈ s, ↑(f a).toNNRat

Proof state:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(f x).toNNRat

Tactic:
rw [Rat.coe_toNNRat _ (hf x hxs)]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∏ i ∈ s, f i = ∏ a ∈ s, ↑(f a).toNNRat

Tactic:
exact Finset.prod_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem alter_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : Option (β k) → Option (β k)} :
    m.alter k f = Raw₀.alter ⟨m, h.size_buckets_pos⟩ k f

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
k : α
f : Option (β k) → Option (β k)
⊢ m.alter k f = (Raw₀.alter ⟨m, ⋯⟩ k f).val

Tactic:
simp [Raw.alter, h.size_buckets_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
    (m.erase k).getKey? a = if k == a then none else m.getKey? a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
⊢ (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a

Tactic:
simp_to_raw using Raw₀.getKey?_erase

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem ergodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ μ') :
    Ergodic (e ∘ f ∘ e.symm) μ' ↔ Ergodic f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
⊢ MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ

Tactic:
rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ
h : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Tactic:
exact ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with },
  fun hf => { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Tactic:
replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff

Result:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ
h : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Tactic:
have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
  rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]

Result:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma coeff_ΨSq (n : ℤ) : (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = n ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2

Tactic:
induction n using Int.negInduction with
| nat n => exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right
| neg ih => simp_rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.ΨSq ↑n).coeff ((↑n).natAbs ^ 2 - 1) = ↑↑n ^ 2
n✝ : ℕ
⊢ (W.ΨSq (-↑n✝)).coeff ((-↑n✝).natAbs ^ 2 - 1) = ↑(-↑n✝) ^ 2

Tactic:
simp_rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.ΨSq ↑n).coeff ((↑n).natAbs ^ 2 - 1) = ↑↑n ^ 2

Tactic:
exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
lemma Gammaℝ_add_two {s : ℂ} (hs : s ≠ 0) : Gammaℝ (s + 2) = Gammaℝ s * s / 2 / π

Proof state:
s : ℂ
hs : s ≠ 0
⊢ (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / ↑π

Tactic:
rw [Gammaℝ_def, Gammaℝ_def, neg_div, add_div, neg_add, div_self two_ne_zero,
  Gamma_add_one _ (div_ne_zero hs two_ne_zero),
  cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), cpow_neg_one]

Result:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s / 2)) * (↑π)⁻¹ * (s / 2 * Gamma (s / 2)) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π

Proof state:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s / 2)) * (↑π)⁻¹ * (s / 2 * Gamma (s / 2)) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π

Tactic:
field_simp [pi_ne_zero]

Result:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-s / 2) * (s * Gamma (s / 2)) * (2 * ↑π) = ↑π ^ (-s / 2) * Gamma (s / 2) * s * (↑π * 2)

Proof state:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-s / 2) * (s * Gamma (s / 2)) * (2 * ↑π) = ↑π ^ (-s / 2) * Gamma (s / 2) * s * (↑π * 2)

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem lt_size_of_lt_aig_size (aig : AIG α) (input : β aig len) (h : x < aig.decls.size) :
    x < (f aig input).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ x < (f aig input).aig.decls.size

Tactic:
apply Nat.lt_of_lt_of_le

Result:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ x < ?m

case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ Nat

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ x < ?m

Tactic:
exact h

Result:
no goals

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

Tactic:
exact le_size aig input

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem lowerSemicontinuous (s : Set α) :
    LowerSemicontinuous fun f : α →ᵤ[s.image singleton] E => eVariationOn f s := fun f ↦ by
  apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E (s.image singleton)) id (𝓝 f) f s _
  simpa only [UniformOnFun.tendsto_iff_tendstoUniformlyOn, mem_image, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, tendstoUniformlyOn_singleton_iff_tendsto] using @tendsto_id _ (𝓝 f)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
⊢ LowerSemicontinuousAt (fun f => eVariationOn f s) f

Tactic:
apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E (s.image singleton)) id (𝓝 f) f s _

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))

Tactic:
simpa only [UniformOnFun.tendsto_iff_tendstoUniformlyOn, mem_image, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, tendstoUniformlyOn_singleton_iff_tendsto] using @tendsto_id _ (𝓝 f)

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.exists_pow_eq' (hs : s.Finite) (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
    ∃ n : ℕ, (f ^ n) a = b

Proof state:
case intro.intro.intro
α : Type u_2
f : Perm α
a b : α
s : Finset α
hs : (↑s).Finite
hf : f.IsCycleOn ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
n : ℕ
hn : (f ^ n) a = b
⊢ ∃ n, (f ^ n) a = b

Tactic:
exact ⟨n, hn⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
s : Set α
a b : α
hs : s.Finite
hf : f.IsCycleOn s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n, (f ^ n) a = b

Tactic:
lift s to Finset α using id hs

Result:
case intro
α : Type u_2
f : Perm α
a b : α
s : Finset α
hs : (↑s).Finite
hf : f.IsCycleOn ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ ∃ n, (f ^ n) a = b

Proof state:
case intro
α : Type u_2
f : Perm α
a b : α
s : Finset α
hs : (↑s).Finite
hf : f.IsCycleOn ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ ∃ n, (f ^ n) a = b

Tactic:
obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb

Result:
case intro.intro.intro
α : Type u_2
f : Perm α
a b : α
s : Finset α
hs : (↑s).Finite
hf : f.IsCycleOn ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
n : ℕ
hn : (f ^ n) a = b
⊢ ∃ n, (f ^ n) a = b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
    (h : m.WF) {hc : k' ∈ m.modify k f} :
    (m.modify k f).getKey k' hc =
      if k == k' then
        k
      else
        haveI h' : k' ∈ m := mem_modify h |>.mp hc
        m.getKey k' h'

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
hc : k' ∈ m.modify k f
⊢ (m.modify k f).contains k' = true → (m.modify k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp_to_raw using Raw₀.getKey_modify

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
hc : k' ∈ m.modify k f
⊢ (m.modify k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
hc✝ : k' ∈ m.modify k f
hc : (m.modify k f).contains k' = true
⊢ (m.modify k f).getKey k' hc✝ = if (k == k') = true then k else m.getKey k' ⋯

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
hc✝ : k' ∈ m.modify k f
hc : (m.modify k f).contains k' = true
⊢ (m.modify k f).getKey k' hc✝ = if (k == k') = true then k else m.getKey k' ⋯

Tactic:
revert hc

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
hc : k' ∈ m.modify k f
⊢ (m.modify k f).contains k' = true → (m.modify k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma mapCoeffs_X :
    mapCoeffs (X : A[X]) = 0

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
⊢ mapCoeffs X = 0

Tactic:
simp [← monomial_one_one_eq_X]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma FormalMultilinearSeries.radius_pi_eq_iInf :
    (FormalMultilinearSeries.pi p).radius = ⨅ i, (p i).radius

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ (pi p).radius = ⨅ i, (p i).radius

Tactic:
refine le_antisymm (by simp [radius_pi_le]) ?_

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ ⨅ i, (p i).radius ≤ (pi p).radius

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
r' : ℝ≥0
hr' : ↑r' < ⨅ i, (p i).radius
⊢ ↑r' ≤ (pi p).radius

Tactic:
exact le_radius_pi (fun i ↦ le_iInf_iff.1 hr'.le i)

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ (pi p).radius ≤ ⨅ i, (p i).radius

Tactic:
simp [radius_pi_le]

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ ⨅ i, (p i).radius ≤ (pi p).radius

Tactic:
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
r' : ℝ≥0
hr' : ↑r' < ⨅ i, (p i).radius
⊢ ↑r' ≤ (pi p).radius
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem exists_lsub_cof (o : Ordinal) :
    ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = cof o

Proof state:
o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
exact csInf_mem (cof_lsub_def_nonempty o)

Result:
no goals

Proof state:
o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = o.cof

Tactic:
rw [cof_eq_sInf_lsub]

Result:
o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem map_leftInverse {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.LeftInverse f g) :
    Function.LeftInverse (map f : MvPolynomial σ R → MvPolynomial σ S₁) (map g) := fun X => by
  rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), map_id]

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ →+* R
hf : LeftInverse ⇑f ⇑g
X : MvPolynomial σ S₁
⊢ (map f) ((map g) X) = X

Tactic:
rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), map_id]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_diff_Ico_left (a b c : α) : Ico a b \ Ico a c = Ico (max a c) b

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ c
⊢ Ico a b \ Ico a c = Ico (a ⊔ c) b

Tactic:
ext x

Result:
case inl.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ c
x : α
⊢ x ∈ Ico a b \ Ico a c ↔ x ∈ Ico (a ⊔ c) b

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico a c = Ico (a ⊔ c) b

Tactic:
cases le_total a c with
| inl h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
  exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
| inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]

Result:
no goals

Proof state:
case inl.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ c
x : α
⊢ (a ≤ x ∧ (a ≤ x → c ≤ x)) ∧ x < b ↔ c ≤ x ∧ x < b

Tactic:
exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩

Result:
no goals

Proof state:
case inl.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ c
x : α
⊢ x ∈ Ico a b \ Ico a c ↔ x ∈ Ico (a ⊔ c) b

Tactic:
rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]

Result:
case inl.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ c
x : α
⊢ (a ≤ x ∧ (a ≤ x → c ≤ x)) ∧ x < b ↔ c ≤ x ∧ x < b

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ a
⊢ Ico a b \ Ico a c = Ico (a ⊔ c) b

Tactic:
rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]

Result:
no goals
-- Mathlib/Data/Multiset/Basic.lean
theorem toList_eq_nil {s : Multiset α} : s.toList = [] ↔ s = 0

Proof state:
α : Type u_1
s : Multiset α
⊢ s.toList = [] ↔ s = 0

Tactic:
rw [← coe_eq_zero, coe_toList]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem submodule_span_le_lieSpan : Submodule.span R s ≤ lieSpan R L s

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
⊢ Submodule.span R s ≤ ↑(lieSpan R L s)

Tactic:
rw [Submodule.span_le]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
⊢ s ⊆ ↑↑(lieSpan R L s)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
⊢ s ⊆ ↑↑(lieSpan R L s)

Tactic:
apply subset_lieSpan

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_weightedVSubVSubWeights [DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s) :
    ∑ t ∈ s, weightedVSubVSubWeights k i j t = 0

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ x ∈ s, affineCombinationSingleWeights k i x - ∑ x ∈ s, affineCombinationSingleWeights k j x = 0

Tactic:
simp [hi, hj]

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ t ∈ s, weightedVSubVSubWeights k i j t = 0

Tactic:
simp_rw [weightedVSubVSubWeights, Pi.sub_apply, sum_sub_distrib]

Result:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ x ∈ s, affineCombinationSingleWeights k i x - ∑ x ∈ s, affineCombinationSingleWeights k j x = 0
-- Mathlib/Order/Filter/Prod.lean
theorem prod_inj {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [NeBot f₁] [NeBot g₁] :
    f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
haveI := neBot_of_le hle.1

Result:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : f₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
⊢ f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂

Tactic:
refine ⟨fun h => ?_, fun h => h.1 ▸ h.2 ▸ rfl⟩

Result:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : f₂.NeBot
this : g₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le

Result:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : f₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
haveI := neBot_of_le hle.2

Result:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : f₂.NeBot
this : g₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂
-- Mathlib/Data/List/Infix.lean
theorem insert_eq_ite (a : α) (l : List α) : insert a l = if a ∈ l then l else a :: l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ insert a l = if a ∈ l then l else a :: l

Tactic:
simp only [← elem_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ insert a l = if elem a l = true then l else a :: l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ insert a l = if elem a l = true then l else a :: l

Tactic:
rfl

Result:
no goals