harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
@[simp]
lemma reps_zero_empty : reps 0 = ∅

Proof state:
case intro.intro.intro
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
⊢ False

Tactic:
suffices |A.1 0 1| < 0 by linarith [abs_nonneg (A.1 0 1)]

Result:
case intro.intro.intro
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
⊢ |↑A 0 1| < 0

Proof state:
case intro.intro.intro
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 * ↑A 1 1 = 0
⊢ |↑A 0 1| < 0

Tactic:
simp_all [h₂.ne']

Result:
no goals

Proof state:
case intro.intro.intro
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
⊢ |↑A 0 1| < 0

Tactic:
have := A_c_eq_zero h₁

Result:
case intro.intro.intro
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 * ↑A 1 1 = 0
⊢ |↑A 0 1| < 0

Proof state:
⊢ reps 0 = ∅

Tactic:
rw [reps, Set.eq_empty_iff_forall_not_mem]

Result:
⊢ ∀ (x : FixedDetMatrix (Fin 2) ℤ 0), x ∉ {A | ↑A 1 0 = 0 ∧ 0 < ↑A 0 0 ∧ 0 ≤ ↑A 0 1 ∧ |↑A 0 1| < |↑A 1 1|}

Proof state:
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
this : |↑A 0 1| < 0
⊢ False

Tactic:
linarith [abs_nonneg (A.1 0 1)]

Result:
no goals

Proof state:
⊢ ∀ (x : FixedDetMatrix (Fin 2) ℤ 0), x ∉ {A | ↑A 1 0 = 0 ∧ 0 < ↑A 0 0 ∧ 0 ≤ ↑A 0 1 ∧ |↑A 0 1| < |↑A 1 1|}

Tactic:
rintro A ⟨h₁, h₂, -, h₄⟩

Result:
case intro.intro.intro
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
⊢ False
-- Mathlib/Geometry/Group/Growth/LinearLowerBound.lean
@[to_additive]
lemma pow_right_strictMono (hX₁ : 1 ∈ X) (hXclosure : (closure (X : Set G) : Set G).Infinite) :
    StrictMono fun n ↦ X ^ n

Proof state:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
⊢ StrictMono fun n => X ^ n

Tactic:
have h n : (X ^ (n - 1) : Set G) ≠ closure (X : Set G) :=
  fun h ↦ by simp [← h, ← coe_pow] at hXclosure

Result:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
h : ∀ (n : ℕ), ↑X ^ (n - 1) ≠ ↑(closure ↑X)
⊢ StrictMono fun n => X ^ n

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
n : ℕ
h : ↑X ^ (n - 1) = ↑(closure ↑X)
⊢ False

Tactic:
simp [← h, ← coe_pow] at hXclosure

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
⊢ StrictMono fun n => X ^ n

Tactic:
obtain rfl | hX := eq_singleton_or_nontrivial hX₁

Result:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
hX₁ : 1 ∈ {1}
hXclosure : (↑(closure ↑{1})).Infinite
⊢ StrictMono fun n => {1} ^ n

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
⊢ StrictMono fun n => X ^ n

Proof state:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
h : ∀ (n : ℕ), ↑X ^ (n - 1) ≠ ↑(closure ↑X)
⊢ StrictMono fun n => X ^ n

Tactic:
simpa [h] using pow_right_strictMonoOn hX₁ hX

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
hX₁ : 1 ∈ {1}
hXclosure : (↑(closure ↑{1})).Infinite
⊢ StrictMono fun n => {1} ^ n

Tactic:
simp [closure_singleton_one] at hXclosure

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem tail_support_append {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    (p.append p').support.tail = p.support.tail ++ p'.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').support.tail = p.support.tail ++ p'.support.tail

Tactic:
rw [support_append, List.tail_append_of_ne_nil (support_ne_nil _)]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_finset' {s : Finset α} : a ∈ stabilizer G s ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ s

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Tactic:
simp_rw [← Finset.mem_inv_smul_finset_iff, Finset.subset_iff]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a ∈ stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Tactic:
rw [← Subgroup.inv_mem_iff, mem_stabilizer_finset_iff_subset_smul_finset]

Result:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem lcs_add_le_iff (l k : ℕ) : N₁.lcs (l + k) ≤ N₂ ↔ N₁.lcs l ≤ N₂.ucs k

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
l : ℕ
⊢ lcs (l + 0) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs 0 N₂

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂

Tactic:
rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
l k : ℕ
⊢ lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂

Tactic:
induction k generalizing l with
| zero => simp
| succ k ih =>
  rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ l + (k + 1) = l + 1 + k

Tactic:
abel

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem _root_.Algebra.TensorProduct.isAlgebraic_of_isField
    (A : Type v) [CommRing A] (B : Type w) [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Flat R A] [Module.Flat R B] (H : IsField (A ⊗[R] B)) :
    Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Module.Flat R A
inst✝ : Module.Flat R B
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
⊢ False

Tactic:
obtain ⟨_, _⟩ := h

Result:
case intro
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Module.Flat R A
inst✝ : Module.Flat R B
H : IsField (A ⊗[R] B)
left✝ : Algebra.Transcendental R A
right✝ : Algebra.Transcendental R B
⊢ False

Proof state:
case intro
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Module.Flat R A
inst✝ : Module.Flat R B
H : IsField (A ⊗[R] B)
left✝ : Algebra.Transcendental R A
right✝ : Algebra.Transcendental R B
⊢ False

Tactic:
exact Algebra.TensorProduct.not_isField_of_transcendental R A B H

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Module.Flat R A
inst✝ : Module.Flat R B
H : IsField (A ⊗[R] B)
h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B
⊢ False

Tactic:
simp_rw [← Algebra.transcendental_iff_not_isAlgebraic] at h

Result:
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Module.Flat R A
inst✝ : Module.Flat R B
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
⊢ False

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Module.Flat R A
inst✝ : Module.Flat R B
H : IsField (A ⊗[R] B)
⊢ Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B

Tactic:
by_contra! h

Result:
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Module.Flat R A
inst✝ : Module.Flat R B
H : IsField (A ⊗[R] B)
h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B
⊢ False
-- Mathlib/Analysis/Calculus/FDeriv/WithLp.lean
theorem differentiable_piLp : Differentiable 𝕜 f ↔ ∀ i, Differentiable 𝕜 fun x => f x i

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun x => f x i

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiable_iff, differentiable_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
⊢ (∀ (i : ι), Differentiable 𝕜 fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable 𝕜 fun x => f x i

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
⊢ (∀ (i : ι), Differentiable 𝕜 fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable 𝕜 fun x => f x i

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_inv_hom_hom_hom_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom =
      (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom

Tactic:
simp [← cancel_epi ((α_ f g h).hom ▷ i)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_sq_mul_cos :
    ∫ x in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
have := @integral_sin_pow_mul_cos_pow_odd a b 2 0

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ (2 * 0 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
exact this

Result:
no goals

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ (2 * 0 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
norm_num at this

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
-- Mathlib/CategoryTheory/Localization/Opposite.lean
lemma isoOfHom_unop  {X Y : Cᵒᵖ} (w : X ⟶ Y) (hw : W.op w) :
    (isoOfHom L.op W.op w hw).unop = (isoOfHom L W w.unop hw)

Proof state:
case w
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
⊢ (isoOfHom L.op W.op w hw).unop.hom = (isoOfHom L W w.unop hw).hom

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
⊢ (isoOfHom L.op W.op w hw).unop = isoOfHom L W w.unop hw

Tactic:
ext

Result:
case w
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
⊢ (isoOfHom L.op W.op w hw).unop.hom = (isoOfHom L W w.unop hw).hom
-- Mathlib/Data/Matroid/Closure.lean
lemma isBase_iff_indep_closure_eq : M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E

Proof state:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)

Tactic:
exact fun hI ↦ ⟨fun h ↦ (M.closure_subset_ground _).antisymm h.2,
  fun h ↦ ⟨(M.subset_closure B).trans_eq h, h.symm.subset⟩⟩

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E

Tactic:
rw [← isBasis_ground_iff, isBasis_iff_indep_subset_closure, and_congr_right_iff]

Result:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)
-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem OrthogonalFamily.inner_right_fintype [Fintype ι] (l : ∀ i, G i) (i : ι) (v : G i) :
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ⟪v, l i⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ inner ((V i) v) (∑ j : ι, (V j) (l j)) = ∑ j : ι, inner ((V i) v) ((V j) (l j))

Tactic:
rw [inner_sum]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ inner ((V i) v) (∑ j : ι, (V j) (l j)) = inner v (l i)

Tactic:
calc
  ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
  _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
    (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
  _ = ⟪v, l i⟫ := by
    simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ (∑ j : ι, if i = j then inner ((V i) v) ((V j) (l j)) else 0) = inner v (l i)

Tactic:
simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ inner ((V i) v) (∑ j : ι, (V j) (l j)) = inner v (l i)

Tactic:
classical
calc
  ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
  _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
    (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
  _ = ⟪v, l i⟫ := by
    simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem subtypeVal_diagSub {α : TypeVec n} : subtypeVal (repeatEq α) ⊚ diagSub = prod.diag

Proof state:
case a.h.fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
x : α Fin2.fz
⊢ (subtypeVal α.repeatEq ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x

Tactic:
simp [comp, diagSub, subtypeVal, prod.diag]

Result:
no goals

Proof state:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} (x : α a✝), (subtypeVal α.repeatEq ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec.{u_1} (n✝ + 1)
x : α a✝.fs
⊢ (subtypeVal α.repeatEq ⊚ diagSub) a✝.fs x = prod.diag a✝.fs x

Tactic:
simp only [comp, subtypeVal, diagSub, prod.diag] at *

Result:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} (x : α a✝), subtypeVal α.repeatEq a✝ (diagSub a✝ x) = prod.diag a✝ x
α : TypeVec.{u_1} (n✝ + 1)
x : α a✝.fs
⊢ subtypeVal (dropFun α.repeatEq) a✝ (diagSub a✝ x) = prod.diag a✝ x

Proof state:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} (x : α a✝), subtypeVal α.repeatEq a✝ (diagSub a✝ x) = prod.diag a✝ x
α : TypeVec.{u_1} (n✝ + 1)
x : α a✝.fs
⊢ subtypeVal (dropFun α.repeatEq) a✝ (diagSub a✝ x) = prod.diag a✝ x

Tactic:
apply i_ih

Result:
no goals

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
⊢ (subtypeVal α.repeatEq ⊚ diagSub) i x = prod.diag i x

Tactic:
induction i with
| fz => simp [comp, diagSub, subtypeVal, prod.diag]
| fs _ i_ih =>
  simp only [comp, subtypeVal, diagSub, prod.diag] at *
  apply i_ih

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} n
⊢ subtypeVal α.repeatEq ⊚ diagSub = prod.diag

Tactic:
ext i x

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
⊢ (subtypeVal α.repeatEq ⊚ diagSub) i x = prod.diag i x
-- Mathlib/Data/List/MinMax.lean
theorem coe_le_maximum_iff : a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b

Tactic:
induction' l <;> simp [maximum_cons, *]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem units_smul_of_pos (u : Rˣ) (hu : 0 < (u.1 : R)) (v : Module.Ray R M) : u • v = v

Proof state:
case h
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ SameRay R (u • v✝) v✝

Tactic:
exact SameRay.sameRay_pos_smul_left _ hu

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ u • rayOfNeZero R v✝ hv✝ = rayOfNeZero R v✝ hv✝

Tactic:
rw [smul_rayOfNeZero, ray_eq_iff]

Result:
case h
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ SameRay R (u • v✝) v✝

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v : Ray R M
⊢ u • v = v

Tactic:
induction v using Module.Ray.ind

Result:
case h
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ u • rayOfNeZero R v✝ hv✝ = rayOfNeZero R v✝ hv✝
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem map_jacobson_of_surjective {f : R →+* S} (hf : Function.Surjective f) :
    RingHom.ker f ≤ I → map f I.jacobson = (map f I).jacobson

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
rcases map_eq_top_or_isMaximal_of_surjective f hf hJ.left.right with htop | hmax

Result:
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
hmax : (map f J).IsMaximal
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasDerivAt_rpow_const {x p : ℝ} (h : x ≠ 0 ∨ 1 ≤ p) :
    HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Proof state:
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Tactic:
rcases ne_or_eq x 0 with (hx | rfl)

Result:
case inl
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
hx : x ≠ 0
⊢ HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

case inr
p : ℝ
h : 0 ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0

Proof state:
case inr
p : ℝ
h : 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0

Tactic:
apply hasDerivAt_of_hasDerivAt_of_ne fun x hx =>
  (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt

Result:
case inr.hf
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x => x ^ p) 0

case inr.hg
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x => p * x ^ (p - 1)) 0

Proof state:
case inr
p : ℝ
h : 0 ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0

Tactic:
replace h : 1 ≤ p := h.neg_resolve_left rfl

Result:
case inr
p : ℝ
h : 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0

Proof state:
case inl
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
hx : x ≠ 0
⊢ HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Tactic:
exact (hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt

Result:
no goals

Proof state:
case inr.hf
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x => x ^ p) 0

case inr.hg
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x => p * x ^ (p - 1)) 0

Tactic:
exacts [continuousAt_id.rpow_const (Or.inr (zero_le_one.trans h)),
  continuousAt_const.mul (continuousAt_id.rpow_const (Or.inr (sub_nonneg.2 h)))]

Result:
no goals