harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem Submodule.range_ker_disjoint {f : M →ₗ[R] M'}
    (hv : LinearIndependent R (f ∘ v)) :
    Disjoint (span R (range v)) (LinearMap.ker f)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : LinearIndependent R (⇑f ∘ v)
⊢ Disjoint (span R (range v)) (LinearMap.ker f)

Tactic:
rw [LinearIndependent, Finsupp.linearCombination_linear_comp] at hv

Result:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ Disjoint (span R (range v)) (LinearMap.ker f)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ Disjoint (span R (range v)) (LinearMap.ker f)

Tactic:
rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
  map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
    (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
theorem exists_continuous_nnreal_forall_closedBall_subset (hK : ∀ i, IsClosed (K i))
    (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) :
    ∃ δ : C(X, ℝ≥0), (∀ x, 0 < δ x) ∧ ∀ (i), ∀ x ∈ K i, closedBall x (δ x) ⊆ U i

Proof state:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ EMetric.closedBall x ↑(δ x) ⊆ U i

Tactic:
exact hδ i x hx

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Tactic:
refine ⟨δ, hδ0, fun i x hx => ?_⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ closedBall x ↑(δ x) ⊆ U i

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Tactic:
rcases EMetric.exists_continuous_nnreal_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ0, hδ⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Proof state:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ closedBall x ↑(δ x) ⊆ U i

Tactic:
rw [← emetric_closedBall_nnreal]

Result:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ EMetric.closedBall x ↑(δ x) ⊆ U i
-- Mathlib/ModelTheory/Complexity.lean
theorem iff_toPrenex (φ : L.BoundedFormula α n) :
    φ ⇔[∅] φ.toPrenex := fun M v xs => by
  rw [realize_iff, realize_toPrenex]

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
M : ∅.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ φ.toPrenex).Realize v xs

Tactic:
rw [realize_iff, realize_toPrenex]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem Substructure.cg_iff_structure_cg (S : L.Substructure M) : S.CG ↔ Structure.CG L S

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.CG ↔ ⊤.CG

Tactic:
refine ⟨fun h => CG.of_map_embedding S.subtype ?_, fun h => ?_⟩

Result:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.CG
⊢ (map S.subtype.toHom ⊤).CG

case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.CG
⊢ S.CG

Proof state:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.CG
h : S.CG
⊢ S.CG

Tactic:
exact h

Result:
no goals

Proof state:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.CG
⊢ (map S.subtype.toHom ⊤).CG

Tactic:
rw [← Hom.range_eq_map, range_subtype]

Result:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.CG
⊢ S.CG

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.CG ↔ Structure.CG L ↥S

Tactic:
rw [Structure.cg_def]

Result:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.CG ↔ ⊤.CG

Proof state:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.CG
⊢ S.CG

Tactic:
have h := h.map S.subtype.toHom

Result:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.CG
h : (map S.subtype.toHom ⊤).CG
⊢ S.CG

Proof state:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.CG
⊢ S.CG

Tactic:
exact h

Result:
no goals

Proof state:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.CG
h : (map S.subtype.toHom ⊤).CG
⊢ S.CG

Tactic:
rw [← Hom.range_eq_map, range_subtype] at h

Result:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.CG
h : S.CG
⊢ S.CG
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem head?_attachWith {P : α → Prop} {xs : List α}
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.attachWith P H).head? = xs.head?.pbind (fun a h => some ⟨a, H _ (mem_of_mem_head? h)⟩)

Proof state:
α : Type u_1
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.attachWith P H).head? = xs.head?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
cases xs <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a

Proof state:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ countP p { toList := toList✝ } = 0 ↔ ∀ (a : α✝), a ∈ { toList := toList✝ } → ¬p a = true

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type u_1
l : Array α✝
p : α✝ → Bool
⊢ countP p l = 0 ↔ ∀ (a : α✝), a ∈ l → ¬p a = true

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ countP p { toList := toList✝ } = 0 ↔ ∀ (a : α✝), a ∈ { toList := toList✝ } → ¬p a = true
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.mul_closedBall_one (hs : IsCompact s) (hδ : 0 ≤ δ) :
    s * closedBall (1 : E) δ = cthickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ x ∈ s * closedBall 1 δ ↔ x ∈ ⋃ x ∈ s, closedBall x δ

Proof state:
case h
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ x ∈ s * closedBall 1 δ ↔ x ∈ ⋃ x ∈ s, closedBall x δ

Tactic:
simp only [mem_mul, dist_eq_norm_div, exists_prop, mem_iUnion, mem_closedBall, exists_and_left,
  mem_closedBall_one_iff, ← eq_div_iff_mul_eq'', div_one, exists_eq_right]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s

Tactic:
rw [hs.cthickening_eq_biUnion_closedBall hδ]

Result:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
-- Mathlib/RingTheory/Radical.lean
theorem radical_dvd_self (a : M) : radical a ∣ a

Proof state:
case pos
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a = 0
⊢ radical a ∣ a

Tactic:
rw [ha]

Result:
case pos
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a = 0
⊢ radical 0 ∣ 0

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
⊢ radical a ∣ a

Tactic:
by_cases ha : a = 0

Result:
case pos
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a = 0
⊢ radical a ∣ a

case neg
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ radical a ∣ a

Proof state:
case neg.h
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).val ≤ normalizedFactors a

Tactic:
rw [primeFactors, Multiset.toFinset_val]

Result:
case neg.h
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (normalizedFactors a).dedup ≤ normalizedFactors a

Proof state:
case neg
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ radical a ∣ a

Tactic:
rw [radical, ← Finset.prod_val, ← (prod_normalizedFactors ha).dvd_iff_dvd_right]

Result:
case neg
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).val.prod ∣ (normalizedFactors a).prod

Proof state:
case neg.h
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (normalizedFactors a).dedup ≤ normalizedFactors a

Tactic:
apply Multiset.dedup_le

Result:
no goals

Proof state:
case neg
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).val.prod ∣ (normalizedFactors a).prod

Tactic:
apply Multiset.prod_dvd_prod_of_le

Result:
case neg.h
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).val ≤ normalizedFactors a

Proof state:
case pos
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a = 0
⊢ radical 0 ∣ 0

Tactic:
apply dvd_zero

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem real_smul_negPart_nonneg (r : ℝ) (hr : 0 ≤ r) :
    (r • j).negPart = r.toNNReal • j.negPart

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r • j).negPart = r.toNNReal • j.negPart

Tactic:
rw [real_smul_def, ← smul_negPart, if_pos hr]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem zeroRootSubalgebra_eq_of_is_cartan (H : LieSubalgebra R L) [H.IsCartanSubalgebra]
    [IsNoetherian R L] : zeroRootSubalgebra R L H = H

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
this : rootSpace H 0 ≤ H.toLieSubmodule
⊢ zeroRootSubalgebra R L H ≤ H

Tactic:
exact fun x hx => this hx

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ LieModule.IsNilpotent ↥H ↥(rootSpace H 0)

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
k : ℕ
hk : rootSpace H 0 ≤ LieSubmodule.ucs k ⊥
⊢ rootSpace H 0 ≤ H.toLieSubmodule

Tactic:
exact hk.trans (LieSubmodule.ucs_le_of_normalizer_eq_self (by simp) k)

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
k : ℕ
hk : rootSpace H 0 ≤ LieSubmodule.ucs k ⊥
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ rootSpace H 0 ≤ H.toLieSubmodule

Tactic:
obtain ⟨k, hk⟩ := (rootSpace H 0).isNilpotent_iff_exists_self_le_ucs.mp (by infer_instance)

Result:
case intro
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
k : ℕ
hk : rootSpace H 0 ≤ LieSubmodule.ucs k ⊥
⊢ rootSpace H 0 ≤ H.toLieSubmodule

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ zeroRootSubalgebra R L H ≤ H

Tactic:
suffices rootSpace H 0 ≤ H.toLieSubmodule by exact fun x hx => this hx

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ rootSpace H 0 ≤ H.toLieSubmodule

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ zeroRootSubalgebra R L H = H

Tactic:
refine le_antisymm ?_ (le_zeroRootSubalgebra R L H)

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ zeroRootSubalgebra R L H ≤ H
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem norm_cexp_neg_mul_sq_add_mul_I (b : ℂ) (c T : ℝ) :
    ‖cexp (-b * (T + c * I) ^ 2)‖ = exp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))

Proof state:
b : ℂ
c T : ℝ
⊢ rexp
      (-(b.re * ((T + (c * 0 - 0 * 1)) * (T + (c * 0 - 0 * 1)) - (0 + (c * 1 + 0 * 0)) * (0 + (c * 1 + 0 * 0))) -
          b.im * ((T + (c * 0 - 0 * 1)) * (0 + (c * 1 + 0 * 0)) + (0 + (c * 1 + 0 * 0)) * (T + (c * 0 - 0 * 1))))) =
    rexp (-(b.re * (T * T) - 2 * b.im * c * T - b.re * (c * c)))

Tactic:
ring_nf

Result:
no goals

Proof state:
b : ℂ
c T : ℝ
⊢ rexp (-((↑b.re + ↑b.im * I) * (↑T + ↑c * I) ^ 2).re) =
    rexp (-((↑b.re + ↑b.im * I).re * T ^ 2 - 2 * (↑b.re + ↑b.im * I).im * c * T - (↑b.re + ↑b.im * I).re * c ^ 2))

Tactic:
simp only [sq, re_add_im, mul_re, mul_im, add_re, add_im, ofReal_re, ofReal_im, I_re, I_im]

Result:
b : ℂ
c T : ℝ
⊢ rexp
      (-(b.re * ((T + (c * 0 - 0 * 1)) * (T + (c * 0 - 0 * 1)) - (0 + (c * 1 + 0 * 0)) * (0 + (c * 1 + 0 * 0))) -
          b.im * ((T + (c * 0 - 0 * 1)) * (0 + (c * 1 + 0 * 0)) + (0 + (c * 1 + 0 * 0)) * (T + (c * 0 - 0 * 1))))) =
    rexp (-(b.re * (T * T) - 2 * b.im * c * T - b.re * (c * c)))

Proof state:
b : ℂ
c T : ℝ
⊢ ‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))

Tactic:
rw [Complex.norm_exp, neg_mul, neg_re, ← re_add_im b]

Result:
b : ℂ
c T : ℝ
⊢ rexp (-((↑b.re + ↑b.im * I) * (↑T + ↑c * I) ^ 2).re) =
    rexp (-((↑b.re + ↑b.im * I).re * T ^ 2 - 2 * (↑b.re + ↑b.im * I).im * c * T - (↑b.re + ↑b.im * I).re * c ^ 2))
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem hasSum_geometric_two' (a : ℝ) : HasSum (fun n : ℕ ↦ a / 2 / 2 ^ n) a

Proof state:
a : ℝ
⊢ HasSum (fun n => a / 2 / 2 ^ n) a

Tactic:
convert HasSum.mul_left (a / 2)
    (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1

Result:
case h.e'_5
a : ℝ
⊢ (fun n => a / 2 / 2 ^ n) = fun i => a / 2 * (1 / 2) ^ i

case h.e'_6
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹

Proof state:
case h.e'_5.h
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (1 / 2) ^ n

Tactic:
simp only [one_div, inv_pow]

Result:
case h.e'_5.h
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (2 ^ n)⁻¹

Proof state:
case h.e'_6
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_5
a : ℝ
⊢ (fun n => a / 2 / 2 ^ n) = fun i => a / 2 * (1 / 2) ^ i

Tactic:
funext n

Result:
case h.e'_5.h
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (1 / 2) ^ n

Proof state:
case h.e'_5.h
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (2 ^ n)⁻¹

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le {a b : ℝ} (ha : a ≤ 0) {z : ℂ}
    (hz : |z.im| ≤ b) (hb : b ≤ π / 2) :
    ‖exp (a * (exp z + exp (-z)))‖ ≤ Real.exp (a * Real.cos b * Real.exp |z.re|)

Proof state:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)

Tactic:
have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
  apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re

Result:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)

Proof state:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)

Tactic:
refine mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha

Result:
case refine_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|

case refine_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ 0 ≤ Real.cos b

Proof state:
case refine_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ -(π / 2) ≤ b

Tactic:
exact (neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)

Result:
no goals

Proof state:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ ‖cexp (↑a * (cexp z + cexp (-z)))‖ ≤ rexp (a * Real.cos b * rexp |z.re|)

Tactic:
simp only [norm_exp, Real.exp_le_exp, re_ofReal_mul, add_re, exp_re, neg_im, Real.cos_neg, ←
  add_mul, mul_assoc, mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]

Result:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)

Proof state:
case refine_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ 0 ≤ Real.cos b

Tactic:
refine Real.cos_nonneg_of_mem_Icc ⟨?_, hb⟩

Result:
case refine_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ -(π / 2) ≤ b

Proof state:
case refine_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|

Tactic:
exact
  Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _)
    (hb.trans <| half_le_self <| Real.pi_pos.le) hz

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast!_eq_getLast?_getD [Inhabited α] {l : List α} : getLast! l = (getLast? l).getD default

Proof state:
case nil
α : Type u_1
inst✝ : Inhabited α
⊢ [].getLast! = [].getLast?.getD default

Tactic:
simp [getLast!_nil]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getLast! = (head✝ :: tail✝).getLast?.getD default

Tactic:
simp [getLast!, getLast?_eq_getLast]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ l.getLast! = l.getLast?.getD default

Tactic:
cases l with
| nil => simp [getLast!_nil]
| cons _ _ => simp [getLast!, getLast?_eq_getLast]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
/-- Given any pair of coprime elements of `R`, there exists a matrix in `SL(2, R)` having those
entries as its top or bottom row. -/
lemma exists_SL2_row {a b : R} (hab : IsCoprime a b) (i : Fin 2) :
    ∃ g : SL(2, R), g i 0 = a ∧ g i 1 = b

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
hab : IsCoprime a b
i : Fin 2
⊢ ∃ g, ↑g i 0 = a ∧ ↑g i 1 = b

Tactic:
obtain ⟨u, v, h⟩ := hab

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ ∃ g, ↑g i 0 = a ∧ ↑g i 1 = b

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - -u * a = u * a + v * b

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, -u; a, b].det = 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Result:
case intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - -u * a = u * a + v * b