harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma summable_f_int (k : ℕ) (a : ℝ) {t : ℝ} (ht : 0 < t) : Summable (f_int k a t)

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -(↑m + 1) + a = -(↑m + (1 - a))

Tactic:
ring

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -↑(m + 1) + a = -(↑m + (1 - a))

Tactic:
push_cast

Result:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -(↑m + 1) + a = -(↑m + (1 - a))

Proof state:
case hf
k : ℕ
a t : ℝ
ht : 0 < t
n : ℤ
⊢ ‖f_int k a t n‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖

Tactic:
rcases n with - | m

Result:
case hf.ofNat
k : ℕ
a t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ ‖f_int k a t (Int.ofNat a✝)‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.ofNat a✝)‖

case hf.negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖

Proof state:
case hf
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable fun a_1 => ‖f_int k a t a_1‖

Tactic:
suffices ∀ n, ‖f_int k a t n‖ = ‖(Int.rec (f_nat k a t) (f_nat k (1 - a) t) : ℤ → ℝ) n‖ from
  funext this ▸ (HasSum.int_rec (summable_f_nat k a ht).hasSum
    (summable_f_nat k (1 - a) ht).hasSum).summable.norm

Result:
case hf
k : ℕ
a t : ℝ
ht : 0 < t
⊢ ∀ (n : ℤ), ‖f_int k a t n‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖

Proof state:
case hf
k : ℕ
a t : ℝ
ht : 0 < t
⊢ ∀ (n : ℤ), ‖f_int k a t n‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖

Tactic:
intro n

Result:
case hf
k : ℕ
a t : ℝ
ht : 0 < t
n : ℤ
⊢ ‖f_int k a t n‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖

Proof state:
case hf.ofNat
k : ℕ
a t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ ‖f_int k a t (Int.ofNat a✝)‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.ofNat a✝)‖

Tactic:
simp only [f_int, f_nat, Int.ofNat_eq_coe, Int.cast_natCast, norm_mul, norm_eq_abs, abs_pow,
  abs_abs]

Result:
no goals

Proof state:
case hf.negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖

Tactic:
simp only [f_int, f_nat, Int.cast_negSucc, norm_mul, norm_eq_abs, abs_pow, abs_abs,
  (by { push_cast; ring } : -↑(m + 1) + a = -(m + (1 - a))), abs_neg, neg_sq]

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (f_int k a t)

Tactic:
apply Summable.of_norm

Result:
case hf
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable fun a_1 => ‖f_int k a t a_1‖
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
/-- The `CommGroupWithZero` version of `div_eq_div_iff_div_eq_div`. -/
lemma div_eq_div_iff_div_eq_div' (hb : b ≠ 0) (hc : c ≠ 0) : a / b = c / d ↔ a / c = b / d

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a / c = b / d

Tactic:
conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]

Result:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a = b / d * c

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a = b / d * c

Tactic:
rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]

Result:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a / c = b / d
-- Mathlib/GroupTheory/Finiteness.lean
theorem Submonoid.FG.map {M' : Type*} [Monoid M'] {P : Submonoid M} (h : P.FG) (e : M →* M') :
    (P.map e).FG

Proof state:
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
⊢ (Submonoid.map e P).FG

Tactic:
obtain ⟨s, rfl⟩ := h

Result:
case intro
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ (Submonoid.map e (closure ↑s)).FG

Proof state:
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
⊢ (Submonoid.map e P).FG

Tactic:
classical
  obtain ⟨s, rfl⟩ := h
  exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ (Submonoid.map e (closure ↑s)).FG

Tactic:
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure ↑(Finset.image (⇑e) s) = Submonoid.map e (closure ↑s)

Tactic:
rw [Finset.coe_image, MonoidHom.map_mclosure]

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
theorem CompactlyGeneratedSpace.isOpen [CompactlyGeneratedSpace X] {s : Set X}
    (hs : ∀ ⦃K⦄, IsCompact K → IsOpen (s ∩ K)) : IsOpen s

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen (s ∩ K)
⊢ IsOpen s

Tactic:
refine isOpen' fun K _ _ _ f hf ↦ ?_

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsOpen (f ⁻¹' s)

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsOpen (f ⁻¹' (s ∩ range f))

Tactic:
exact (hs (isCompact_range hf)).preimage hf

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsOpen (f ⁻¹' s)

Tactic:
rw [← Set.preimage_inter_range]

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsOpen (f ⁻¹' (s ∩ range f))
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith [PseudoEMetricSpace α]
    [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β}
    (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : ℝ≥0)
    (ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t)
    (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ EMetric.ball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * ↑(3 * K) + ε / 2

Tactic:
push_cast

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ EMetric.ball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * (3 * ↑K) + ε / 2

Proof state:
case mk.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε

Tactic:
rcases EMetric.mem_closure_iff.1 (hss' hx) δ δpos with ⟨x', hx', hxx'⟩

Result:
case mk.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
-- Mathlib/Logic/Nontrivial/Defs.lean
theorem Function.Surjective.nontrivial [Nontrivial β] {f : α → β}
    (hf : Function.Surjective f) : Nontrivial α

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
this : x' ≠ y'
⊢ Nontrivial α

Tactic:
exact ⟨⟨x', y', this⟩⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α

Tactic:
have : x' ≠ y' := by
  refine fun H ↦ h ?_
  rw [← hx', ← hy', H]

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
this : x' ≠ y'
⊢ Nontrivial α

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α

Tactic:
rcases hf x with ⟨x', hx'⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
⊢ Nontrivial α

Tactic:
rcases exists_pair_ne β with ⟨x, y, h⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y

Tactic:
rw [← hx', ← hy', H]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α

Tactic:
rcases hf y with ⟨y', hy'⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ x' ≠ y'

Tactic:
refine fun H ↦ h ?_

Result:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y
-- Mathlib/Computability/TMToPartrec.lean
theorem trStmts₁_self (q) : q ∈ trStmts₁ q

Proof state:
case ret
k✝ : Cont'
⊢ Λ'.ret k✝ ∈ trStmts₁ (Λ'.ret k✝)

Tactic:
first |apply Finset.mem_singleton_self|apply Finset.mem_insert_self

Result:
no goals

Proof state:
case ret
k✝ : Cont'
⊢ Λ'.ret k✝ ∈ trStmts₁ (Λ'.ret k✝)

Tactic:
apply Finset.mem_singleton_self

Result:
no goals

Proof state:
case pred
q₁✝ q₂✝ : Λ'
q₁_ih✝ : q₁✝ ∈ trStmts₁ q₁✝
q₂_ih✝ : q₂✝ ∈ trStmts₁ q₂✝
⊢ q₁✝.pred q₂✝ ∈ trStmts₁ (q₁✝.pred q₂✝)

Tactic:
apply Finset.mem_insert_self

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem exists_path_through_family' {n : ℕ} (p : Fin (n + 1) → X) :
    ∃ (γ : Path (p 0) (p n)) (t : Fin (n + 1) → I), ∀ i, γ (t i) = p i

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p ↑n)
t : Fin (n + 1) → ↑I
h : ∀ (i : Fin (n + 1)), γ (t i) = p i
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
exact ⟨γ, t, h⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
rcases this.exists_path_through_family' p fun _i => True.intro with ⟨γ, t, -, h⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p ↑n)
t : Fin (n + 1) → ↑I
h : ∀ (i : Fin (n + 1)), γ (t i) = p i
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ PathConnectedSpace X

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_lemma (n k : ℕ) (h : ¬n < k * k) : sqrt n - k < sqrt n + 2 - k :=
  (Nat.sub_lt_sub_right <| le_sqrt.2 <| le_of_not_gt h) <| Nat.lt_add_of_pos_right (by decide)

Proof state:
n k : ℕ
h : ¬n < k * k
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_diff_Iio : Iio b \ Iio a = Ico a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Iio b \ Iio a = Ico a b

Tactic:
rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iio]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Prod.lean
theorem isLinearMap_add [AddCommMonoid M] [Module R M] :
    IsLinearMap R fun x : M × M => x.1 + x.2

Proof state:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)

Tactic:
simp only [Prod.fst_add, Prod.snd_add]

Result:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ x.1 + y.1 + (x.2 + y.2) = x.1 + x.2 + (y.1 + y.2)

Proof state:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)

Tactic:
intro x y

Result:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsLinearMap R fun x => x.1 + x.2

Tactic:
apply IsLinearMap.mk

Result:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)

case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 + (c • x).2 = c • (x.1 + x.2)

Proof state:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ x.1 + y.1 + (x.2 + y.2) = x.1 + x.2 + (y.1 + y.2)

Tactic:
abel

Result:
no goals

Proof state:
case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 + (c • x).2 = c • (x.1 + x.2)

Tactic:
intro x y

Result:
case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
y : M × M
⊢ (x • y).1 + (x • y).2 = x • (y.1 + y.2)

Proof state:
case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
y : M × M
⊢ (x • y).1 + (x • y).2 = x • (y.1 + y.2)

Tactic:
simp [smul_add]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalComp_cons_nil {f f' g g' h i : C}
    {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {β : f' ≅ g'}
    {η₁ : g ⊗ g' ⟶ h ⊗ g'} {ηs₁ : h ⊗ g' ⟶ i ⊗ g'} {η₂ : g ⊗ g' ⟶ i ⊗ g'} {η₃ : f ⊗ f' ⟶ i ⊗ g'}
    (e_η₁ : ((Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom) ▷ g' = η₁) (e_ηs₁ : ηs ▷ g' = ηs₁)
    (e_η₂ : η₁ ≫ ηs₁ = η₂) (e_η₃ : (α ⊗ β).hom ≫ η₂ = η₃) :
    (α.hom ≫ η ≫ ηs) ⊗ β.hom = η₃

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
η₁ : g ⊗ g' ⟶ h ⊗ g'
ηs₁ : h ⊗ g' ⟶ i ⊗ g'
η₂ : g ⊗ g' ⟶ i ⊗ g'
η₃ : f ⊗ f' ⟶ i ⊗ g'
e_η₁ : ((Iso.refl g).hom ≫ η ≫ (Iso.refl h).hom) ▷ g' = η₁
e_ηs₁ : ηs ▷ g' = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ⊗ β).hom ≫ η₂ = η₃
⊢ α.hom ≫ η ≫ ηs ⊗ β.hom = η₃

Tactic:
simp_all [MonoidalCategory.tensorHom_def']

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem card_classGroup_eq_one [IsPrincipalIdealRing R] : Fintype.card (ClassGroup R) = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∃ x, ∀ (y : ClassGroup R), y = x

Tactic:
use 1

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∀ (y : ClassGroup R), y = 1

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∀ (y : ClassGroup R), y = 1

Tactic:
refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ClassGroup.mk I = 1

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ClassGroup.mk I = 1

Tactic:
exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ Fintype.card (ClassGroup R) = 1

Tactic:
rw [Fintype.card_eq_one_iff]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∃ x, ∀ (y : ClassGroup R), y = x
-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma subset_mul_closure_one {G} [MulOneClass G] [TopologicalSpace G] (s : Set G) :
    s ⊆ s * (closure {1} : Set G)

Proof state:
G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
⊢ s ⊆ s * closure {1}

Tactic:
have : s ⊆ s * ({1} : Set G) := by simp

Result:
G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
this : s ⊆ s * {1}
⊢ s ⊆ s * closure {1}

Proof state:
G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
this : s ⊆ s * {1}
⊢ s ⊆ s * closure {1}

Tactic:
exact this.trans (smul_subset_smul_left subset_closure)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
⊢ s ⊆ s * {1}

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
theorem hasSum_int_hurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℤ ↦ SignType.sign (n + a) / (↑|n + a| : ℂ) ^ s / 2) (hurwitzZetaOdd a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 =
    (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 / (s + 1).Gammaℝ

Tactic:
have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 =
    (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 / (s + 1).Gammaℝ

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (hurwitzZetaOdd (↑a) s)

Tactic:
refine ((hasSum_int_completedHurwitzZetaOdd a hs).div_const (Gammaℝ _)).congr_fun fun n ↦ ?_

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 =
    (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 / (s + 1).Gammaℝ

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < s.re + 1

Tactic:
positivity

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < (s + 1).re

Tactic:
rw [add_re, one_re]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < s.re + 1

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 =
    (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 / (s + 1).Gammaℝ

Tactic:
simp [div_right_comm _ _ (Gammaℝ _), mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
@[simp] lemma finsuppAntidiag_empty_zero : finsuppAntidiag (∅ : Finset ι) (0 : μ) = {0}

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
f : ι →₀ μ
⊢ f ∈ ∅.finsuppAntidiag 0 ↔ f ∈ {0}

Tactic:
simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), eq_comm]

Result:
no goals

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
⊢ ∅.finsuppAntidiag 0 = {0}

Tactic:
ext f

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
f : ι →₀ μ
⊢ f ∈ ∅.finsuppAntidiag 0 ↔ f ∈ {0}
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_neighborSet {n : ℕ} {v : Fin (n + 2)} :
    (cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1}

Proof state:
case h
n : ℕ
v w : Fin (n + 2)
⊢ (cycleGraph (n + 2)).Adj v w ↔ w = v - 1 ∨ w = v + 1

Tactic:
rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]

Result:
no goals

Proof state:
n : ℕ
v : Fin (n + 2)
⊢ (cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1}

Tactic:
ext w

Result:
case h
n : ℕ
v w : Fin (n + 2)
⊢ w ∈ (cycleGraph (n + 2)).neighborSet v ↔ w ∈ {v - 1, v + 1}

Proof state:
case h
n : ℕ
v w : Fin (n + 2)
⊢ w ∈ (cycleGraph (n + 2)).neighborSet v ↔ w ∈ {v - 1, v + 1}

Tactic:
simp only [mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff]

Result:
case h
n : ℕ
v w : Fin (n + 2)
⊢ (cycleGraph (n + 2)).Adj v w ↔ w = v - 1 ∨ w = v + 1