harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem coeff_inv_aux [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) :
    coeff R n (inv.aux a φ) =
      if n = 0 then a
      else
        -a *
          ∑ x ∈ antidiagonal n, if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 :=
  show inv.aux a φ n = _ by
    cases Subsingleton.elim ‹DecidableEq σ› (Classical.decEq σ)
    rw [inv.aux]
    rfl

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ inv.aux a φ n =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0

Tactic:
cases Subsingleton.elim ‹DecidableEq σ› (Classical.decEq σ)

Result:
case refl
σ : Type u_1
R : Type u_2
inst✝ : Ring R
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ inv.aux a φ n =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0

Proof state:
case refl
σ : Type u_1
R : Type u_2
inst✝ : Ring R
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ inv.aux a φ n =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0

Tactic:
rw [inv.aux]

Result:
case refl
σ : Type u_1
R : Type u_2
inst✝ : Ring R
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ (if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x_1 : x.2 < n then (coeff R x.1) φ * inv.aux a φ x.2 else 0) =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0

Proof state:
case refl
σ : Type u_1
R : Type u_2
inst✝ : Ring R
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ (if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x_1 : x.2 < n then (coeff R x.1) φ * inv.aux a φ x.2 else 0) =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
theorem not_isUnit_of_natDegree_pos_of_isReduced [IsReduced R] (p : R[X])
    (hpl : 0 < p.natDegree) : ¬ IsUnit p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
⊢ ¬IsUnit p

Tactic:
simp only [ne_eq, isNilpotent_iff_eq_zero, not_and, not_forall, exists_prop,
  Polynomial.isUnit_iff_coeff_isUnit_isNilpotent]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
⊢ IsUnit (p.coeff 0) → ∃ x, ¬x = 0 ∧ ¬p.coeff x = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
a✝ : IsUnit (p.coeff 0)
hpl : p.coeff p.natDegree = 0
⊢ p.natDegree ≤ 0

Tactic:
simp only [coeff_natDegree, leadingCoeff_eq_zero] at hpl

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
a✝ : IsUnit (p.coeff 0)
hpl : p = 0
⊢ p.natDegree ≤ 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
⊢ IsUnit (p.coeff 0) → ∃ x, ¬x = 0 ∧ ¬p.coeff x = 0

Tactic:
intro _

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
a✝ : IsUnit (p.coeff 0)
⊢ ∃ x, ¬x = 0 ∧ ¬p.coeff x = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
a✝ : IsUnit (p.coeff 0)
⊢ ∃ x, ¬x = 0 ∧ ¬p.coeff x = 0

Tactic:
refine ⟨p.natDegree, hpl.ne', ?_⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
a✝ : IsUnit (p.coeff 0)
⊢ ¬p.coeff p.natDegree = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
a✝ : IsUnit (p.coeff 0)
⊢ ¬p.coeff p.natDegree = 0

Tactic:
contrapose! hpl

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
a✝ : IsUnit (p.coeff 0)
hpl : p.coeff p.natDegree = 0
⊢ p.natDegree ≤ 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
a✝ : IsUnit (p.coeff 0)
hpl : p = 0
⊢ p.natDegree ≤ 0

Tactic:
simp [hpl]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Lattice.lean
theorem eq_top_iff_one : I = ⊤ ↔ (1 : α) ∈ I :=
  ⟨by rintro rfl; trivial, fun h => eq_top_of_unit_mem _ _ 1 h (by simp)⟩

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ I = ⊤ → 1 ∈ I

Tactic:
rintro rfl

Result:
α : Type u
inst✝ : Semiring α
⊢ 1 ∈ ⊤

Proof state:
α : Type u
inst✝ : Semiring α
⊢ 1 ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
h : 1 ∈ I
⊢ 1 * 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/DenselyOrdered.lean
@[to_additive]
lemma le_mul_of_forall_lt [CommGroup α] [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
    [DenselyOrdered α] {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') :
    c ≤ a * b

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd✝ : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d

Tactic:
obtain ⟨b', hb', hd⟩ := exists_mul_right_lt hd

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd✝¹ : a * b < d
a' : α
ha' : a' > a
hd✝ : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Proof state:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Result:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd : a * b < d
⊢ c ≤ d

Proof state:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd : a * b < d
⊢ c ≤ d

Tactic:
obtain ⟨a', ha', hd⟩ := exists_mul_left_lt hd

Result:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd✝ : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd✝¹ : a * b < d
a' : α
ha' : a' > a
hd✝ : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' ha' b' hb').trans hd.le

Result:
no goals
-- Mathlib/NumberTheory/PrimeCounting.lean
@[simp]
lemma primeCounting_eq_zero_iff {n : ℕ} : n.primeCounting = 0 ↔ n ≤ 1

Proof state:
n : ℕ
⊢ π n = 0 ↔ n ≤ 1

Tactic:
simp [primeCounting]

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive (attr := simp) Even.nsmul_left]
lemma Even.isSquare_pow : Even n → ∀ a : α, IsSquare (a ^ n)

Proof state:
case intro
α : Type u_2
inst✝ : Monoid α
m : ℕ
a : α
⊢ IsSquare (a ^ (m + m))

Tactic:
exact ⟨a ^ m, pow_add _ _ _⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Monoid α
n : ℕ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)

Tactic:
rintro ⟨m, rfl⟩ a

Result:
case intro
α : Type u_2
inst✝ : Monoid α
m : ℕ
a : α
⊢ IsSquare (a ^ (m + m))
-- Mathlib/SetTheory/Game/PGame.lean
theorem add_lf_add_right {y z : PGame} (h : y ⧏ z) (x) : y + x ⧏ z + x :=
  suffices z + x ≤ y + x → z ≤ y by
    rw [← PGame.not_le] at h ⊢
    exact mt this h
  fun w =>
  calc
    z ≤ z + 0 := (PGame.add_zero _).symm.le
    _ ≤ z + (x + -x) := add_le_add_left (zero_le_add_neg_cancel x) _
    _ ≤ z + x + -x := (PGame.add_assoc _ _ _).symm.le
    _ ≤ y + x + -x := add_le_add_right w _
    _ ≤ y + (x + -x) := (PGame.add_assoc _ _ _).le
    _ ≤ y + 0 := add_le_add_left (add_neg_cancel_le_zero x) _
    _ ≤ y := (PGame.add_zero _).le

Proof state:
y z : PGame
h : ¬z ≤ y
x : PGame
this : z + x ≤ y + x → z ≤ y
⊢ ¬z + x ≤ y + x

Tactic:
exact mt this h

Result:
no goals

Proof state:
y z : PGame
h : y ⧏ z
x : PGame
this : z + x ≤ y + x → z ≤ y
⊢ y + x ⧏ z + x

Tactic:
rw [← PGame.not_le] at h ⊢

Result:
y z : PGame
h : ¬z ≤ y
x : PGame
this : z + x ≤ y + x → z ≤ y
⊢ ¬z + x ≤ y + x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs

Proof state:
α : Type u_1
as✝ bs cs✝ : List α
a : α
as : List α
c : α
cs : List α
h₁ : a = c
h₂ : as.append bs = cs.append bs
⊢ a :: as = c :: cs

Tactic:
subst h₁

Result:
α : Type u_1
as✝ bs cs✝ : List α
a : α
as cs : List α
h₂ : as.append bs = cs.append bs
⊢ a :: as = a :: cs

Proof state:
α : Type u_1
as✝ bs cs✝ : List α
a : α
as cs : List α
h₂ : as.append bs = cs.append bs
⊢ a :: as = a :: cs

Tactic:
rw [append_cancel_right h₂]

Result:
no goals

Proof state:
α : Type u_1
as bs cs✝ : List α
c : α
cs : List α
h : [] ++ bs = c :: cs ++ bs
⊢ [] = c :: cs

Tactic:
have aux := congrArg length h

Result:
α : Type u_1
as bs cs✝ : List α
c : α
cs : List α
h : [] ++ bs = c :: cs ++ bs
aux : ([] ++ bs).length = (c :: cs ++ bs).length
⊢ [] = c :: cs

Proof state:
α : Type u_1
as bs cs✝ : List α
c : α
cs : List α
h : [] ++ bs = c :: cs ++ bs
aux : ([] ++ bs).length = (c :: cs ++ bs).length
⊢ [] = c :: cs

Tactic:
simp_arith at aux

Result:
no goals

Proof state:
α : Type u_1
as✝ bs cs : List α
a : α
as : List α
h : a :: as ++ bs = [] ++ bs
⊢ a :: as = []

Tactic:
have aux := congrArg length h

Result:
α : Type u_1
as✝ bs cs : List α
a : α
as : List α
h : a :: as ++ bs = [] ++ bs
aux : (a :: as ++ bs).length = ([] ++ bs).length
⊢ a :: as = []

Proof state:
α : Type u_1
as✝ bs cs : List α
a : α
as : List α
h : a :: as ++ bs = [] ++ bs
aux : (a :: as ++ bs).length = ([] ++ bs).length
⊢ a :: as = []

Tactic:
simp_arith at aux

Result:
no goals

Proof state:
α : Type u_1
as bs cs : List α
h : as ++ bs = cs ++ bs
⊢ as = cs

Tactic:
match as, cs with
| [], []       => rfl
| [], c::cs    => have aux := congrArg length h; simp_arith at aux
| a::as, []    => have aux := congrArg length h; simp_arith at aux
| a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]

Result:
no goals

Proof state:
α : Type u_1
as✝ bs cs✝ : List α
a : α
as : List α
c : α
cs : List α
h : a :: as ++ bs = c :: cs ++ bs
⊢ a :: as = c :: cs

Tactic:
injection h with h₁ h₂

Result:
α : Type u_1
as✝ bs cs✝ : List α
a : α
as : List α
c : α
cs : List α
h₁ : a = c
h₂ : as.append bs = cs.append bs
⊢ a :: as = c :: cs

Proof state:
α : Type u_1
as bs cs : List α
h : [] ++ bs = [] ++ bs
⊢ [] = []

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙHom_of_cfcHom_map_quasispectrum {a : A} (ha : p a) :
    ∀ f : C(σₙ R a, R)₀, σₙ R (cfcₙHom_of_cfcHom R ha f) = range f

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ spectrum R
        (((↑(cfcHom ha)).comp
            ((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom))
          f) ∪
      {0} =
    range ⇑f

Tactic:
simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply,
  NonUnitalStarAlgHom.coe_coe]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ spectrum R
        ((cfcHom ha)
          ((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f))) ∪
      {0} =
    range ⇑f

Proof state:
case h.mpr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : R
⊢ x ∈ range ⇑f →
    x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0}

Tactic:
rintro ⟨x, rfl⟩

Result:
case h.mpr.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : ↑(σₙ R a)
⊢ f x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0}

Proof state:
case h.mp.inl.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : ↑(spectrum R a)
⊢ ((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) x ∈ range ⇑f

Tactic:
exact ⟨⟨x.1, spectrum_subset_quasispectrum R a x.2⟩, rfl⟩

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem mem_prod_iff {s : Set (α × β)} {f : Filter α} {g : Filter β} :
    s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Proof state:
case mp
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Tactic:
rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1 ∈ f, ∃ t₂_1 ∈ g, t₁_1 ×ˢ t₂_1 ⊆ t₁ ∩ t₂

Proof state:
case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g

Tactic:
rintro ⟨t₁, ht₁, t₂, ht₂, h⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : t₁ ×ˢ t₂ ⊆ s
⊢ s ∈ f ×ˢ g

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1 ∈ f, ∃ t₂_1 ∈ g, t₁_1 ×ˢ t₂_1 ⊆ t₁ ∩ t₂

Tactic:
exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : t₁ ×ˢ t₂ ⊆ s
⊢ s ∈ f ×ˢ g

Tactic:
exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma hasSum_expZeta_of_one_lt_re (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ cexp (2 * π * I * a * n) / n ^ s) (expZeta a s)

Proof state:
case h.e'_5.h
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (Complex.cos (2 * ↑π * ↑a * ↑n) + Complex.sin (2 * ↑π * ↑a * ↑n) * I) / ↑n ^ s =
    Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s + I * (Complex.sin (2 * ↑π * ↑a * ↑n) / ↑n ^ s)

Tactic:
rw [add_div, mul_div, mul_comm _ I]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) (expZeta (↑a) s)

Tactic:
convert (hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I) using 1

Result:
case h.e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) = fun b =>
    ↑(Real.cos (2 * π * a * ↑b)) / ↑b ^ s + I * (↑(Real.sin (2 * π * a * ↑b)) / ↑b ^ s)

Proof state:
case h.e'_5.h
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s =
    ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s + I * (↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s)

Tactic:
simp only [mul_right_comm _ I, ← cos_add_sin_I, push_cast]

Result:
case h.e'_5.h
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (Complex.cos (2 * ↑π * ↑a * ↑n) + Complex.sin (2 * ↑π * ↑a * ↑n) * I) / ↑n ^ s =
    Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s + I * (Complex.sin (2 * ↑π * ↑a * ↑n) / ↑n ^ s)

Proof state:
case h.e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) = fun b =>
    ↑(Real.cos (2 * π * a * ↑b)) / ↑b ^ s + I * (↑(Real.sin (2 * π * a * ↑b)) / ↑b ^ s)

Tactic:
ext1 n

Result:
case h.e'_5.h
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s =
    ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s + I * (↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s)
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma mapEmbedding_indep_iff {f : α ↪ β} {I : Set β} :
    (M.mapEmbedding f).Indep I ↔ M.Indep (f ⁻¹' I) ∧ I ⊆ range f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f ⁻¹' (⇑f '' I)) ∧ ⇑f '' I ⊆ range ⇑f

Tactic:
rw [preimage_image_eq _ f.injective]

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f

Tactic:
exact ⟨hI, image_subset_range _ _⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
rw [mapEmbedding, map_indep_iff]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
rintro ⟨I, hI, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f ⁻¹' (⇑f '' I)) ∧ ⇑f '' I ⊆ range ⇑f

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
x✝ : M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
h : M.Indep (⇑f ⁻¹' I)
h' : I ⊆ range ⇑f
⊢ I = ⇑f '' (⇑f ⁻¹' I)

Tactic:
rwa [eq_comm, image_preimage_eq_iff]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem univ_filter_mem_range (f : α → β) [Fintype β] [DecidablePred fun y => y ∈ Set.range f]
    [DecidableEq β] : (Finset.univ.filter fun y => y ∈ Set.range f) = Finset.univ.image f

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
this : DecidablePred fun y => ∃ x, f x = y := inst✝¹
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ

Tactic:
exact univ_filter_exists f

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
⊢ DecidablePred fun y => ∃ x, f x = y

Tactic:
simpa using ‹_›

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ

Tactic:
letI : DecidablePred (fun y => ∃ x, f x = y) := by simpa using ‹_›

Result:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
this : DecidablePred fun y => ∃ x, f x = y := inst✝¹
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem unsat_relabel_iff {f : CNF α} {r : α → β}
    (hw : ∀ {v1 v2}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2) :
    Unsat (relabel r f) ↔ Unsat f

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
⊢ f.Unsat

Tactic:
let g : β → α := fun b =>
  if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
⊢ f.Unsat

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
r : α → β
n : Nat
hw : ∀ {v1 v2 : α}, Mem v1 (List.replicate n []) → Mem v2 (List.replicate n []) → r v1 = r v2 → v1 = v2
⊢ (relabel r (List.replicate n [])).Unsat ↔ Unsat (List.replicate n [])

Tactic:
cases n <;> simp [unsat_def, List.replicate_succ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ g (r v) = v

Tactic:
dsimp [g]

Result:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ (if h : ∃ a, Mem a f ∧ r a = r v then h.choose else a₀) = v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_reverse (l : Array α) (f : α → β → β) (b) :
    l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
  (foldl_reverse ..).symm.trans <| by simp

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β → β
b : β
⊢ foldl (fun y x => f x y) b l.reverse.reverse = foldl (fun x y => f y x) b l

Tactic:
simp

Result:
no goals