harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma coweightEquiv_mul {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
    coweightEquiv P P x * coweightEquiv P P y = coweightEquiv P P y ≪≫ₗ coweightEquiv P P x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
⊢ coweightEquiv P P x * coweightEquiv P P y = coweightEquiv P P y ≪≫ₗ coweightEquiv P P x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
@[to_additive]
lemma tprod_subtype_le {κ γ : Type*} [OrderedCommGroup γ] [UniformSpace γ] [UniformGroup γ]
    [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ a : κ, 1 ≤ f a)
    (hf : Multipliable f) : (∏' (b : β), f b) ≤ (∏' (a : κ), f a)

Proof state:
κ : Type u_4
γ : Type u_5
inst✝⁴ : OrderedCommGroup γ
inst✝³ : UniformSpace γ
inst✝² : UniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a

Tactic:
apply tprod_le_tprod_of_inj _
  (Subtype.coe_injective)
  (by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, h, implies_true])
  (by simp only [le_refl, Subtype.forall, implies_true])
  (by apply hf.subtype)

Result:
κ : Type u_4
γ : Type u_5
inst✝⁴ : OrderedCommGroup γ
inst✝³ : UniformSpace γ
inst✝² : UniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable fun a => f a

Proof state:
κ : Type u_4
γ : Type u_5
inst✝⁴ : OrderedCommGroup γ
inst✝³ : UniformSpace γ
inst✝² : UniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable fun a => f a

Tactic:
apply hf

Result:
no goals

Proof state:
κ : Type u_4
γ : Type u_5
inst✝⁴ : OrderedCommGroup γ
inst✝³ : UniformSpace γ
inst✝² : UniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ (i : { x // x ∈ β }), f ↑i ≤ f ↑i

Tactic:
simp only [le_refl, Subtype.forall, implies_true]

Result:
no goals

Proof state:
κ : Type u_4
γ : Type u_5
inst✝⁴ : OrderedCommGroup γ
inst✝³ : UniformSpace γ
inst✝² : UniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ c ∉ Set.range fun a => ↑a, 1 ≤ f c

Tactic:
simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, h, implies_true]

Result:
no goals

Proof state:
κ : Type u_4
γ : Type u_5
inst✝⁴ : OrderedCommGroup γ
inst✝³ : UniformSpace γ
inst✝² : UniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable fun b => f ↑b

Tactic:
apply hf.subtype

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyInjective.lean
lemma isLocallyInjective_iff_injective :
    IsLocallyInjective φ ↔ ∀ (X : Cᵒᵖ), Function.Injective (φ.val.app X) :=
  Presheaf.isLocallyInjective_iff_injective_of_separated _ _ (by
    apply Presieve.isSeparated_of_isSheaf
    rw [← isSheaf_iff_isSheaf_of_type]
    exact ((sheafCompose J (forget D)).obj F₁).2)

Proof state:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
⊢ Presieve.IsSheaf J (F₁.val ⋙ forget D)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Result:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
⊢ Presheaf.IsSheaf J (F₁.val ⋙ forget D)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
⊢ Presieve.IsSeparated J (F₁.val ⋙ forget D)

Tactic:
apply Presieve.isSeparated_of_isSheaf

Result:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
⊢ Presieve.IsSheaf J (F₁.val ⋙ forget D)

Proof state:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
⊢ Presheaf.IsSheaf J (F₁.val ⋙ forget D)

Tactic:
exact ((sheafCompose J (forget D)).obj F₁).2

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_finset_biUnion_congr {s : Finset ι} {t : ι → Set α} :
    μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔
      ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
induction' s using Finset.induction_on with i s _ hs

Result:
case empty
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
⊢ μ.restrict (⋃ i ∈ ∅, t i) = ν.restrict (⋃ i ∈ ∅, t i) ↔ ∀ i ∈ ∅, μ.restrict (t i) = ν.restrict (t i)

case insert
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
⊢ μ.restrict (⋃ i_1 ∈ insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ insert i s, t i_1) ↔
    ∀ i_1 ∈ insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)

Proof state:
case empty
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
⊢ μ.restrict (⋃ i ∈ ∅, t i) = ν.restrict (⋃ i ∈ ∅, t i) ↔ ∀ i ∈ ∅, μ.restrict (t i) = ν.restrict (t i)

Tactic:
simp

Result:
no goals

Proof state:
case insert
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
⊢ μ.restrict (t i ∪ ⋃ x ∈ s, t x) = ν.restrict (t i ∪ ⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)

Tactic:
rw [restrict_union_congr, ← hs]

Result:
no goals

Proof state:
case insert
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
⊢ μ.restrict (⋃ i_1 ∈ insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ insert i s, t i_1) ↔
    ∀ i_1 ∈ insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)

Tactic:
simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]

Result:
case insert
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
⊢ μ.restrict (t i ∪ ⋃ x ∈ s, t x) = ν.restrict (t i ∪ ⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsupp'_symm_single_eq_single_one_tmul (i : ι × κ) (r : R) :
    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) =
      Finsupp.single i.1 1 ⊗ₜ Finsupp.single i.2 r

Proof state:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (1 * r)) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r

Tactic:
exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Result:
no goals

Proof state:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r

Tactic:
nth_rw 1 [← one_mul r]

Result:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (1 * r)) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r
-- Mathlib/NumberTheory/Pell.lean
theorem exists_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) :
    ∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q => (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Tactic:
have hd₂ : m ∣ q₁.num * q₂.den - q₂.num * q₁.den := by
  rw [← Int.natAbs_dvd, ← ZMod.intCast_eq_intCast_iff_dvd_sub]
  push_cast
  rw [hq1, hq2]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q => (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
-- Mathlib/Order/Interval/Finset/Nat.lean
lemma mem_Ioc_succ : a ∈ Ioc b (b + 1) ↔ a = b + 1

Proof state:
a b : ℕ
⊢ a ∈ Ioc b (b + 1) ↔ a = b + 1

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem Nat.eq_sq_add_sq_of_isSquare_mod_neg_one {n : ℕ} (h : IsSquare (-1 : ZMod n)) :
    ∃ x y : ℕ, n = x ^ 2 + y ^ 2

Proof state:
case h
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Tactic:
haveI : Fact p.Prime := ⟨hpp⟩

Result:
case h
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Proof state:
case h₀
h : IsSquare (-1)
⊢ ∃ x y, 0 = x ^ 2 + y ^ 2

Tactic:
exact ⟨0, 0, rfl⟩

Result:
no goals

Proof state:
case h
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Tactic:
have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h

Result:
case h
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Proof state:
case h₁
h : IsSquare (-1)
⊢ ∃ x y, 1 = x ^ 2 + y ^ 2

Tactic:
exact ⟨0, 1, rfl⟩

Result:
no goals

Proof state:
case h
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Tactic:
obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)

Result:
case h.intro.intro
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Proof state:
case h.intro.intro
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Tactic:
obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)

Result:
case h.intro.intro.intro.intro
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
x y : ℕ
hxy : n = x ^ 2 + y ^ 2
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Proof state:
n : ℕ
h : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
induction n using induction_on_primes with
| h₀ => exact ⟨0, 0, rfl⟩
| h₁ => exact ⟨0, 1, rfl⟩
| h p n hpp ih =>
  haveI : Fact p.Prime := ⟨hpp⟩
  have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
  obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
  obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
  exact Nat.sq_add_sq_mul huv.symm hxy

Result:
no goals

Proof state:
case h.intro.intro.intro.intro
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
x y : ℕ
hxy : n = x ^ 2 + y ^ 2
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Tactic:
exact Nat.sq_add_sq_mul huv.symm hxy

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem norm_add_eq_add_norm_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x + y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2

Tactic:
linarith

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x + y‖ = ‖x‖ + ‖y‖
⊢ angle x y = 0

Tactic:
rw [← inner_eq_mul_norm_iff_angle_eq_zero hx hy]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x + y‖ = ‖x‖ + ‖y‖
⊢ inner x y = ‖x‖ * ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0

Tactic:
refine ⟨fun h => ?_, norm_add_eq_add_norm_of_angle_eq_zero⟩

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x + y‖ = ‖x‖ + ‖y‖
⊢ angle x y = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x + y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = ‖x‖ * ‖y‖

Tactic:
calc
  ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
  _ = ‖x‖ * ‖y‖ := by ring

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x + y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 = ‖x‖ * ‖y‖

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x + y‖ = ‖x‖ + ‖y‖
⊢ inner x y = ‖x‖ * ‖y‖

Tactic:
obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x + y), add_nonneg (norm_nonneg x) (norm_nonneg y)

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x + y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x + y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = ‖x‖ * ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x + y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x + y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = ‖x‖ * ‖y‖

Tactic:
rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_add_pow_two_real] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x + y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = ‖x‖ * ‖y‖
-- Mathlib/Algebra/RingQuot.lean
theorem eq_liftAlgHom_comp_mkAlgHom {s : A → A → Prop} (f : RingQuot s →ₐ[S] B) :
    f = liftAlgHom S ⟨f.comp (mkAlgHom S s), fun _ _ h ↦ congr_arg f (mkAlgHom_rel S h)⟩

Proof state:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : RingQuot s →ₐ[S] B
⊢ { toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
      ({ toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }.symm
        f) =
    { toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      ⟨f.comp (mkAlgHom S s), ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : RingQuot s →ₐ[S] B
⊢ (liftAlgHom S) ((liftAlgHom S).symm f) = (liftAlgHom S) ⟨f.comp (mkAlgHom S s), ⋯⟩

Tactic:
rw [liftAlgHom]

Result:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : RingQuot s →ₐ[S] B
⊢ { toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
      ({ toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }.symm
        f) =
    { toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      ⟨f.comp (mkAlgHom S s), ⋯⟩

Proof state:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : RingQuot s →ₐ[S] B
⊢ f = (liftAlgHom S) ⟨f.comp (mkAlgHom S s), ⋯⟩

Tactic:
conv_lhs => rw [← (liftAlgHom S).apply_symm_apply f]

Result:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : RingQuot s →ₐ[S] B
⊢ (liftAlgHom S) ((liftAlgHom S).symm f) = (liftAlgHom S) ⟨f.comp (mkAlgHom S s), ⋯⟩
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma completedCosZeta₀_neg (a : UnitAddCircle) (s : ℂ) :
    completedCosZeta₀ (-a) s = completedCosZeta₀ a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta₀ (-a) s = completedCosZeta₀ a s

Tactic:
simp [completedCosZeta₀]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_apply_pi {ι : Type*} (f : ι → R → R) (a : A) (ha : p a

Proof state:
case h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) _auto✝
i : ι
⊢ cfc (f i) a = (cfcHom ha) { toFun := (spectrum R a).restrict (f i), continuous_toFun := ⋯ }

Tactic:
simp only [cfc_apply (f i) a ha (hf i)]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) _auto✝
⊢ (fun i => cfc (f i) a) = fun i => (cfcHom ha) { toFun := (spectrum R a).restrict (f i), continuous_toFun := ⋯ }

Tactic:
ext i

Result:
case h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) _auto✝
i : ι
⊢ cfc (f i) a = (cfcHom ha) { toFun := (spectrum R a).restrict (f i), continuous_toFun := ⋯ }
-- Mathlib/MeasureTheory/SetSemiring.lean
theorem iUnion_le_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n ∈ C) (n : ℕ) :
    (⋃ i ≤ n, s i) ∈ C

Proof state:
case zero
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
⊢ ⋃ i, ⋃ (_ : i ≤ 0), s i ∈ C

Tactic:
simp [hs 0]

Result:
no goals

Proof state:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ i, ⋃ (_ : i ≤ n), s i ∈ C
⊢ ⋃ i, ⋃ (_ : i ≤ n + 1), s i ∈ C

Tactic:
rw [biUnion_le_succ]

Result:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ i, ⋃ (_ : i ≤ n), s i ∈ C
⊢ (⋃ k, ⋃ (_ : k ≤ n), s k) ∪ s (n + 1) ∈ C

Proof state:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ i, ⋃ (_ : i ≤ n), s i ∈ C
⊢ (⋃ k, ⋃ (_ : k ≤ n), s k) ∪ s (n + 1) ∈ C

Tactic:
exact hC.union_mem hn (hs _)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
⊢ ⋃ i, ⋃ (_ : i ≤ n), s i ∈ C

Tactic:
induction n with
| zero => simp [hs 0]
| succ n hn => rw [biUnion_le_succ]; exact hC.union_mem hn (hs _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
    getKey (m.insertIfNew k v) a h₁ =
      if h₂ : k == a ∧ ¬k ∈ m then k else getKey m a (mem_of_mem_insertIfNew' h₁ h₂)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).getKey a h₁ = if h : (k == a) = true ∧ m.contains k = false then k else m.getKey a ⋯

Tactic:
exact Raw₀.getKey_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then k else m.getKey a ⋯

Tactic:
simp [mem_iff_contains, contains_insertIfNew]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).getKey a h₁ = if h : (k == a) = true ∧ m.contains k = false then k else m.getKey a ⋯