harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesAt.add (hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) :
    HasFPowerSeriesAt (f + g) (pf + pg) x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x

Proof state:
case intro
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x

Tactic:
exact ⟨r, hr.1.add hr.2⟩

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem mem_avoid : c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Proof state:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ (∃ x ∈ P.parts, ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Tactic:
refine exists_congr fun d ↦ and_congr_right' <| and_congr_left ?_

Result:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
d : α
⊢ d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)

Proof state:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Tactic:
simp only [avoid, ofErase, mem_erase, Ne, mem_image, exists_prop, ← exists_and_left,
  @and_left_comm (c ≠ ⊥)]

Result:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ (∃ x ∈ P.parts, ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Proof state:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b

Tactic:
rw [sdiff_eq_bot_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
d : α
⊢ d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem mul_assoc (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => antidiagonal a.1,
      (coeff R x.snd.1) φ₁ * (coeff R x.snd.2) φ₂ * (coeff R x.fst.2) φ₃ =
    ∑ x ∈ (antidiagonal n).sigma fun a => antidiagonal a.2,
      (coeff R x.fst.1) φ₁ * ((coeff R x.snd.1) φ₂ * (coeff R x.snd.2) φ₃)

Tactic:
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
  (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;> aesop (add simp [add_assoc, mul_assoc])

Result:
no goals

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ₁ * φ₂ * φ₃) = (coeff R n) (φ₁ * (φ₂ * φ₃))

Tactic:
classical
simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
  (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;> aesop (add simp [add_assoc, mul_assoc])

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
⊢ φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)

Tactic:
ext1 n

Result:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ₁ * φ₂ * φ₃) = (coeff R n) (φ₁ * (φ₂ * φ₃))

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ₁ * φ₂ * φ₃) = (coeff R n) (φ₁ * (φ₂ * φ₃))

Tactic:
simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']

Result:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => antidiagonal a.1,
      (coeff R x.snd.1) φ₁ * (coeff R x.snd.2) φ₂ * (coeff R x.fst.2) φ₃ =
    ∑ x ∈ (antidiagonal n).sigma fun a => antidiagonal a.2,
      (coeff R x.fst.1) φ₁ * ((coeff R x.snd.1) φ₂ * (coeff R x.snd.2) φ₃)
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma Icc_chartedSpaceChartAt_of_le_top {z : Set.Icc x y} (h : z.val < y) :
    chartAt _ z = IccLeftChart x y

Proof state:
x y : ℝ
hxy : Fact (x < y)
z : ↑(Icc x y)
h : ↑z < y
⊢ chartAt (EuclideanHalfSpace 1) z = IccLeftChart x y

Tactic:
simp [Icc_chartedSpaceChartAt, h]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem to_subbox_aux (h : Integrable I l f vol) (hJ : J ≤ I) :
    ∃ y : F, HasIntegral J l f vol y ∧
      Tendsto (integralSum f vol) (l.toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 y)

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
y : F
hy : Tendsto (integralSum f vol) (toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 y)
⊢ HasIntegral J l f vol y

Tactic:
convert hy.comp (l.tendsto_embedBox_toFilteriUnion_top hJ)

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
⊢ ∃ y, HasIntegral J l f vol y ∧ Tendsto (integralSum f vol) (toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 y)

Tactic:
refine (cauchy_map_iff_exists_tendsto.1
  (h.cauchy_map_integralSum_toFilteriUnion (.single I J hJ))).imp fun y hy ↦ ⟨?_, hy⟩

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
y : F
hy : Tendsto (integralSum f vol) (toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 y)
⊢ HasIntegral J l f vol y
-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_sup [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α} :
    (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r :=
  Finset.cons_induction_on s (by simp) fun a s ha hs => by simp [-sup_set_eq_biUnion, hs]

Proof state:
ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
⊢ ((cons a s ha).sup f).WellFoundedOn r ↔ ∀ i ∈ cons a s ha, (f i).WellFoundedOn r

Tactic:
simp [-sup_set_eq_biUnion, hs]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ (∅.sup f).WellFoundedOn r ↔ ∀ i ∈ ∅, (f i).WellFoundedOn r

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma conjExponent_eq : conjExponent p = q

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : 1 ≤ p
⊢ p.conjExponent = q

Tactic:
have : p⁻¹ ≠ ∞ := by simpa using h.ne_zero

Result:
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : 1 ≤ p
this : p⁻¹ ≠ ⊤
⊢ p.conjExponent = q

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ p.conjExponent = q

Tactic:
have hp : 1 ≤ p := h.one_le

Result:
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : 1 ≤ p
⊢ p.conjExponent = q

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : 1 ≤ p
this : p⁻¹ ≠ ⊤
⊢ p.conjExponent = q

Tactic:
simpa [ENNReal.add_right_inj, *] using
  (IsConjExponent.conjExponent hp).inv_add_inv_conj.trans h.inv_add_inv_conj.symm

Result:
no goals

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : 1 ≤ p
⊢ p⁻¹ ≠ ⊤

Tactic:
simpa using h.ne_zero

Result:
no goals
-- Mathlib/Algebra/Group/TypeTags/Basic.lean
lemma Pi.mulSingle_multiplicativeOfAdd_eq {ι : Type*} [DecidableEq ι] {M : ι → Type*}
    [(i : ι) → AddMonoid (M i)] (i : ι) (a : M i) (j : ι) :
    Pi.mulSingle (f := fun i ↦ Multiplicative (M i)) i (Multiplicative.ofAdd a) j =
      Multiplicative.ofAdd ((Pi.single i a) j)

Proof state:
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
rcases eq_or_ne j i with rfl | h

Result:
case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
j : ι
a : M j
⊢ mulSingle j (ofAdd a) j = ofAdd (single j a j)

case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Proof state:
case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
j : ι
a : M j
⊢ mulSingle j (ofAdd a) j = ofAdd (single j a j)

Tactic:
simp only [mulSingle_eq_same, single_eq_same]

Result:
no goals

Proof state:
case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
simp only [mulSingle, ne_eq, h, not_false_eq_true, Function.update_of_ne, one_apply, single,
  zero_apply, ofAdd_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma expDegree_rec (m : ℕ) :
    (expDegree (2 * (m + 3)) = 2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5) ∧
    expDegree (2 * (m + 3)) = expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4)) ∧
    (expDegree (2 * (m + 2) + 1) =
      expDegree (m + 4) + 3 * expDegree (m + 2) + (if Even m then 2 * 3 else 0) ∧
    expDegree (2 * (m + 2) + 1) =
      expDegree (m + 1) + 3 * expDegree (m + 3) + (if Even m then 0 else 2 * 3))

Proof state:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    (2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by omega]

Result:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    ((↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6

Proof state:
m : ℕ
⊢ 2 * m + 4 + 1 ≠ 0

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem mixedEmbedding_apply_isComplex (x : K) (w : {w // IsComplex w}) :
    (mixedEmbedding K x).2 w = w.val.embedding x

Proof state:
K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 w = (↑w).embedding x

Tactic:
simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem mem_prod_principal {s : Set (α × β)} :
    s ∈ f ×ˢ 𝓟 t ↔ { a | ∀ b ∈ t, (a, b) ∈ s } ∈ f

Proof state:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s

Tactic:
exact hv (mk_mem_prod a_in <| v_in b_in)

Result:
no goals

Proof state:
case refine_2.mk.intro
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
x : α
y : β
hx : (x, y).1 ∈ u
hy : (x, y).2 ∈ t
⊢ (x, y) ∈ s

Tactic:
exact h hx y hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}

Tactic:
refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
⊢ (∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}

case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f

Tactic:
rw [← @exists_mem_subset_iff _ f, mem_prod_iff]

Result:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}

Proof state:
case refine_1
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
⊢ (∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}

Tactic:
rintro ⟨v, v_in, hv⟩ a a_in b b_in

Result:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s

Proof state:
case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s

Tactic:
rintro ⟨x, y⟩ ⟨hx, hy⟩

Result:
case refine_2.mk.intro
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
x : α
y : β
hx : (x, y).1 ∈ u
hy : (x, y).2 ∈ t
⊢ (x, y) ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_atom {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size}
    (h : (relabel r aig).decls[idx]'hidx = .atom a) :
    ∃ x, aig.decls[idx]'(by rw [← relabel_size_eq_size (r := r)]; omega) = .atom x ∧ a = r x

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.atom a
x : α
⊢ idx < (relabel r aig).decls.size

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.atom a
⊢ Decl.relabel r aig.decls[idx] = Decl.atom a

Tactic:
simpa [relabel] using h

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.atom a
x : α
⊢ idx < aig.decls.size

Tactic:
rw [← relabel_size_eq_size (r := r)]

Result:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.atom a
x : α
⊢ idx < (relabel r aig).decls.size

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.atom a
⊢ ∃ x, aig.decls[idx] = Decl.atom x ∧ a = r x

Tactic:
apply Decl.relabel_atom

Result:
case h
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.atom a
⊢ Decl.relabel r aig.decls[idx] = Decl.atom a
-- Mathlib/Combinatorics/Quiver/Basic.lean
@[simp]
lemma homOfEq_trans {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y')
    {X'' Y'' : V} (hX' : X' = X'') (hY' : Y' = Y'') :
    homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f (hX.trans hX') (hY.trans hY')

Proof state:
V : Type u_1
inst✝ : Quiver V
X Y : V
f : X ⟶ Y
⊢ homOfEq (homOfEq f ⋯ ⋯) ⋯ ⋯ = homOfEq f ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
inst✝ : Quiver V
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : V
hX' : X' = X''
hY' : Y' = Y''
⊢ homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f ⋯ ⋯

Tactic:
subst hX hY hX' hY'

Result:
V : Type u_1
inst✝ : Quiver V
X Y : V
f : X ⟶ Y
⊢ homOfEq (homOfEq f ⋯ ⋯) ⋯ ⋯ = homOfEq f ⋯ ⋯
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma exists_ne_zero (χ : Weight R L M) :
    ∃ x ∈ genWeightSpace M χ, x ≠ 0

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : Weight R L M
⊢ ∃ x ∈ genWeightSpace M ⇑χ, x ≠ 0

Tactic:
simpa [LieSubmodule.eq_bot_iff] using χ.genWeightSpace_ne_bot

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] :
    ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
  | [], a₁, a₂ => rfl
  | a :: l, a₁, a₂ => by
    simp only [foldr_cons, ha.assoc]
    rw [foldr_assoc]

Proof state:
α : Type u_1
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ foldr op (op a₁ a₂) (a :: l) = op (foldr op a₁ (a :: l)) a₂

Tactic:
simp only [foldr_cons, ha.assoc]

Result:
α : Type u_1
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ op a (foldr op (op a₁ a₂) l) = op a (op (foldr op a₁ l) a₂)

Proof state:
α : Type u_1
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ op a (foldr op (op a₁ a₂) l) = op a (op (foldr op a₁ l) a₂)

Tactic:
rw [foldr_assoc]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem finrank (hirr : Irreducible (cyclotomic n K)) : finrank K L = (n : ℕ).totient

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ Module.finrank K L = φ ↑n

Tactic:
rw [((zeta_spec n K L).powerBasis K).finrank, IsPrimitiveRoot.powerBasis_dim, ←
  (zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]

Result:
no goals

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
⊢ Module.finrank K L = φ ↑n

Tactic:
haveI := IsCyclotomicExtension.neZero' n K L

Result:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ Module.finrank K L = φ ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem one_mul : ∀ a : Int, 1 * a = a
  | ofNat n => show ofNat (1 * n) = ofNat n by rw [Nat.one_mul]
  | -[n+1]  => show -[1 * n +1] = -[n+1] by rw [Nat.one_mul]

Proof state:
n : Nat
⊢ -[1 * n+1] = -[n+1]

Tactic:
rw [Nat.one_mul]

Result:
no goals

Proof state:
n : Nat
⊢ ofNat (1 * n) = ofNat n

Tactic:
rw [Nat.one_mul]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma min_left_comm (a b c : ℕ) : min a (min b c) = min b (min a c)

Proof state:
a b c : ℕ
⊢ min a (min b c) = min b (min a c)

Tactic:
rw [← Nat.min_assoc, ← Nat.min_assoc, b.min_comm]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem frobenius_pow {p : ℕ} [Fact p.Prime] [CharP K p] {n : ℕ} (hcard : q = p ^ n) :
    frobenius K p ^ n = 1

Proof state:
case a
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (frobenius K p ^ n) x = x ^ p ^ n

Tactic:
induction n with
| zero => simp
| succ n hn =>
  rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]

Result:
no goals

Proof state:
case a.zero
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ (frobenius K p ^ 0) x = x ^ p ^ 0

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
⊢ frobenius K p ^ n = 1

Tactic:
ext x

Result:
case a
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ (frobenius K p ^ n) x = 1 x

Proof state:
case a
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ (frobenius K p ^ n) x = 1 x

Tactic:
conv_rhs => rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]

Result:
case a
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ (frobenius K p ^ n) x = x ^ p ^ n

Proof state:
case a.succ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : (frobenius K p ^ n) x = x ^ p ^ n
⊢ (frobenius K p ^ (n + 1)) x = x ^ p ^ (n + 1)

Tactic:
rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]

Result:
no goals

Proof state:
case a
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ (frobenius K p ^ n) x = x ^ p ^ n

Tactic:
clear hcard

Result:
case a
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (frobenius K p ^ n) x = x ^ p ^ n
-- Mathlib/Algebra/Order/Module/Algebra.lean
lemma algebraMap_pos (ha : 0 < a) : 0 < algebraMap α β a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : OrderedCommSemiring α
inst✝² : StrictOrderedSemiring β
inst✝¹ : Algebra α β
inst✝ : SMulPosStrictMono α β
a : α
ha : 0 < a
⊢ 0 < (algebraMap α β) a

Tactic:
simpa using algebraMap_strictMono β ha

Result:
no goals