harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Update.lean
theorem _root_.DependsOn.updateFinset {α : Type*} {f : (Π i, π i) → α} {s : Set ι}
    (hf : DependsOn f s) {t : Finset ι} (y : Π i : t, π i) :
    DependsOn (fun x ↦ f (updateFinset x t y)) (s \ t)

Proof state:
case neg
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∉ t
⊢ x₁ i = x₂ i

Tactic:
simp_all

Result:
no goals

Proof state:
case pos
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∈ t
⊢ y ⟨i, h✝⟩ = y ⟨i, h✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
⊢ Function.updateFinset x₁ t y i = Function.updateFinset x₂ t y i

Tactic:
simp only [Function.updateFinset]

Result:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
⊢ (if hi : i ∈ t then y ⟨i, hi⟩ else x₁ i) = if hi : i ∈ t then y ⟨i, hi⟩ else x₂ i

Proof state:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
⊢ (if hi : i ∈ t then y ⟨i, hi⟩ else x₁ i) = if hi : i ∈ t then y ⟨i, hi⟩ else x₂ i

Tactic:
split_ifs

Result:
case pos
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∈ t
⊢ y ⟨i, h✝⟩ = y ⟨i, h✝⟩

case neg
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∉ t
⊢ x₁ i = x₂ i

Proof state:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
⊢ DependsOn (fun x => f (Function.updateFinset x t y)) (s \ ↑t)

Tactic:
refine fun x₁ x₂ h ↦ hf (fun i hi ↦ ?_)

Result:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : { x // x ∈ t }) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
⊢ Function.updateFinset x₁ t y i = Function.updateFinset x₂ t y i
-- Mathlib/NumberTheory/JacobiSum/Basic.lean
theorem jacobiSum_one_nontrivial {χ : MulChar F R} (hχ : χ ≠ 1) : jacobiSum 1 χ = -1

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ jacobiSum 1 χ = -1

Tactic:
have : ∑ x ∈ univ \ {0, 1}, ((1 : MulChar F R) x - 1) * (χ (1 - x) - 1) = 0 := by
  apply Finset.sum_eq_zero
  simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton,
    not_or, ← isUnit_iff_ne_zero, true_and, MulChar.one_apply, sub_self, zero_mul, and_imp,
    implies_true]

Result:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
this : ∑ x ∈ univ \ {0, 1}, (1 x - 1) * (χ (1 - x) - 1) = 0
⊢ jacobiSum 1 χ = -1

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
this : ∑ x ∈ univ \ {0, 1}, (1 x - 1) * (χ (1 - x) - 1) = 0
⊢ jacobiSum 1 χ = -1

Tactic:
simp only [jacobiSum_eq_aux, MulChar.sum_one_eq_card_units, MulChar.sum_eq_zero_of_ne_one hχ,
  add_zero, Fintype.card_eq_card_units_add_one (α := F), Nat.cast_add, Nat.cast_one,
  sub_add_cancel_left, this]

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ jacobiSum 1 χ = -1

Tactic:
classical
have : ∑ x ∈ univ \ {0, 1}, ((1 : MulChar F R) x - 1) * (χ (1 - x) - 1) = 0 := by
  apply Finset.sum_eq_zero
  simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton,
    not_or, ← isUnit_iff_ne_zero, true_and, MulChar.one_apply, sub_self, zero_mul, and_imp,
    implies_true]
simp only [jacobiSum_eq_aux, MulChar.sum_one_eq_card_units, MulChar.sum_eq_zero_of_ne_one hχ,
  add_zero, Fintype.card_eq_card_units_add_one (α := F), Nat.cast_add, Nat.cast_one,
  sub_add_cancel_left, this]

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x ∈ univ \ {0, 1}, (1 x - 1) * (χ (1 - x) - 1) = 0

Tactic:
apply Finset.sum_eq_zero

Result:
case h
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∀ x ∈ univ \ {0, 1}, (1 x - 1) * (χ (1 - x) - 1) = 0

Proof state:
case h
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∀ x ∈ univ \ {0, 1}, (1 x - 1) * (χ (1 - x) - 1) = 0

Tactic:
simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton,
  not_or, ← isUnit_iff_ne_zero, true_and, MulChar.one_apply, sub_self, zero_mul, and_imp,
  implies_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem concat_inj {a b : α} {l l' : List α} : concat l a = concat l' b ↔ l = l' ∧ a = b :=
  ⟨fun h => ⟨init_eq_of_concat_eq h, last_eq_of_concat_eq h⟩, by rintro ⟨rfl, rfl⟩; rfl⟩

Proof state:
α : Type u_1
a b : α
l l' : List α
⊢ l = l' ∧ a = b → l.concat a = l'.concat b

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
α : Type u_1
a : α
l : List α
⊢ l.concat a = l.concat a

Proof state:
case intro
α : Type u_1
a : α
l : List α
⊢ l.concat a = l.concat a

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem triangle_assoc_comp_right_inv (f : a ⟶ b) (g : b ⟶ c) :
    (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv

Tactic:
simp [← cancel_mono (f ◁ (λ_ g).hom)]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDerivWithin_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F) (s : Set E) :
    iteratedFDerivWithin 𝕜 n (fun _ : E ↦ c) s = 0

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
s : Set E
n : ℕ
hn : n + 1 ≠ 0
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s = 0

Tactic:
exact iteratedFDerivWithin_succ_const n c

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : n ≠ 0
c : F
s : Set E
⊢ iteratedFDerivWithin 𝕜 n (fun x => c) s = 0

Tactic:
cases n with
| zero => contradiction
| succ n => exact iteratedFDerivWithin_succ_const n c

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
s : Set E
hn : 0 ≠ 0
⊢ iteratedFDerivWithin 𝕜 0 (fun x => c) s = 0

Tactic:
contradiction

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma map_one_one : map F f 1 1 (by simp) = F.map (𝟙 _) := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.84683, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
⊢ 1 ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₁_fst {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G)
    (p : YonedaCollection F X) : (YonedaCollection.map₁ η p).fst = p.fst

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).fst = p.fst

Tactic:
simp [map₁]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformlyOn.congr_right {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : s.EqOn f g) : TendstoLocallyUniformlyOn F g p s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
⊢ TendstoLocallyUniformlyOn F g p s

Tactic:
rintro u hu x hx

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, F n y) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s ∩ t, (g y, F n y) ∈ u

Tactic:
filter_upwards [h] with i hi y hy using hg hy.1 ▸ hi y hy.2

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, F n y) ∈ u

Tactic:
refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin ht, ?_⟩

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s ∩ t, (g y, F n y) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, F n y) ∈ u

Tactic:
obtain ⟨t, ht, h⟩ := hf u hu x hx

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, F n y) ∈ u
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma continuousOn_sinKernel (a : UnitAddCircle) : ContinuousOn (sinKernel a) (Ioi 0)

Proof state:
case H
a : ℝ
⊢ ContinuousOn (fun x => ↑(sinKernel (↑a) x)) (Ioi 0)

Tactic:
simp_rw [sinKernel_def]

Result:
case H
a : ℝ
⊢ ContinuousOn (fun x => jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)) (Ioi 0)

Proof state:
case H
a : ℝ
⊢ ContinuousOn (fun x => jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)) (Ioi 0)

Tactic:
apply (continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)).div_const

Result:
a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a) (I * ↑x)) x

Proof state:
a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a) (I * ↑x)) x

Tactic:
have h := continuousAt_jacobiTheta₂' a (by rwa [I_mul_im, ofReal_re])

Result:
a x : ℝ
hx : x ∈ Ioi 0
h : ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (↑a, I * ↑x)
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a) (I * ↑x)) x

Proof state:
case H
a : ℝ
⊢ ContinuousOn (sinKernel ↑a) (Ioi 0)

Tactic:
suffices ContinuousOn (fun x ↦ (sinKernel a x : ℂ)) (Ioi 0) from
  (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm

Result:
case H
a : ℝ
⊢ ContinuousOn (fun x => ↑(sinKernel (↑a) x)) (Ioi 0)

Proof state:
a x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < im ?m.70923

Tactic:
rwa [I_mul_im, ofReal_re]

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ ContinuousOn (sinKernel a) (Ioi 0)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a =>
suffices ContinuousOn (fun x ↦ (sinKernel a x : ℂ)) (Ioi 0) from
  (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
simp_rw [sinKernel_def]
apply (continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)).div_const
have h := continuousAt_jacobiTheta₂' a (by rwa [I_mul_im, ofReal_re])
fun_prop

Result:
no goals

Proof state:
a x : ℝ
hx : x ∈ Ioi 0
h : ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (↑a, I * ↑x)
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a) (I * ↑x)) x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.diff_singleton_isBasis (hC : M.IsCircuit C) (he : e ∈ C) :
    M.IsBasis (C \ {e}) C

Proof state:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) (insert e C)

Tactic:
rw [← insert_diff_singleton, (hC.diff_singleton_indep he).isBasis_insert_iff,
  insert_diff_singleton, insert_eq_of_mem he]

Result:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}

Proof state:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
nth_rw 2 [← insert_eq_of_mem he]

Result:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) (insert e C)

Proof state:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}

Tactic:
exact Or.inl hC.dep

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem mem_skewAdjointMatricesSubmodule' :
    A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A

Proof state:
R₂ : Type u_3
inst✝² : CommRing R₂
n : Type u_5
inst✝¹ : Fintype n
J A : Matrix n n R₂
inst✝ : DecidableEq n
⊢ A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A

Tactic:
simp only [mem_skewAdjointMatricesSubmodule]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem length_eraseIdx_add_one {l : List ι} {i : ℕ} (h : i < l.length) :
    (l.eraseIdx i).length + 1 = l.length

Proof state:
ι : Type u_1
l : List ι
i : ℕ
h : i < l.length
⊢ (if i < l.length then l.length - 1 else l.length) + 1 = l.length

Tactic:
split <;> omega

Result:
no goals

Proof state:
ι : Type u_1
l : List ι
i : ℕ
h : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length

Tactic:
rw [length_eraseIdx]

Result:
ι : Type u_1
l : List ι
i : ℕ
h : i < l.length
⊢ (if i < l.length then l.length - 1 else l.length) + 1 = l.length
-- Mathlib/Analysis/Normed/Algebra/Unitization.lean
lemma norm_inr (a : A) : ‖(a : Unitization 𝕜 A)‖ = ‖a‖

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
a : A
⊢ ‖↑a‖ = ‖a‖

Tactic:
simp [norm_eq_sup]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsReal.comp (f : k →+* K) {φ : K →+* ℂ} (hφ : IsReal φ) :
    IsReal (φ.comp f)

Proof state:
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
⊢ IsReal (φ.comp f)

Tactic:
ext1 x

Result:
case a
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ (star (φ.comp f)) x = (φ.comp f) x

Proof state:
case a
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ (star (φ.comp f)) x = (φ.comp f) x

Tactic:
simpa using RingHom.congr_fun hφ (f x)

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem congr_symm (e : M ≃ₗ[R] M') : (congr e).symm = congr e.symm

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_7
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
⊢ (congr e).symm = congr e.symm

Tactic:
ext

Result:
case h.H
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_7
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
x✝¹ : BilinForm R M'
x✝ y✝ : M
⊢ (((congr e).symm x✝¹) x✝) y✝ = (((congr e.symm) x✝¹) x✝) y✝

Proof state:
case h.H
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_7
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
x✝¹ : BilinForm R M'
x✝ y✝ : M
⊢ (((congr e).symm x✝¹) x✝) y✝ = (x✝¹ (e x✝)) (e y✝)

Tactic:
rfl

Result:
no goals

Proof state:
case h.H
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_7
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
x✝¹ : BilinForm R M'
x✝ y✝ : M
⊢ (((congr e).symm x✝¹) x✝) y✝ = (((congr e.symm) x✝¹) x✝) y✝

Tactic:
simp only [congr_apply, LinearEquiv.symm_symm]

Result:
case h.H
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_7
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
x✝¹ : BilinForm R M'
x✝ y✝ : M
⊢ (((congr e).symm x✝¹) x✝) y✝ = (x✝¹ (e x✝)) (e y✝)
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem idealFactorsFunOfQuotHom_comp {f : R ⧸ I →+* A ⧸ J} {g : A ⧸ J →+* B ⧸ L}
    (hf : Function.Surjective f) (hg : Function.Surjective g) :
    (idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) =
      idealFactorsFunOfQuotHom (show Function.Surjective (g.comp f) from hg.comp hf)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
⊢ (idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) = idealFactorsFunOfQuotHom ⋯

Tactic:
refine OrderHom.ext _ _ (funext fun x => ?_)

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ((idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf)) x = (idealFactorsFunOfQuotHom ⋯) x

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ((idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf)) x = (idealFactorsFunOfQuotHom ⋯) x

Tactic:
rw [idealFactorsFunOfQuotHom, idealFactorsFunOfQuotHom, OrderHom.comp_coe, OrderHom.coe_mk,
  OrderHom.coe_mk, Function.comp_apply, idealFactorsFunOfQuotHom, OrderHom.coe_mk,
  Subtype.mk_eq_mk, Subtype.coe_mk, map_comap_of_surjective (Ideal.Quotient.mk J)
  Ideal.Quotient.mk_surjective, map_map]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_add (f : M → N) (x y : M) :
    f (x + y) = f x + f y + polar f x y

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + (f (x + y) - f x - f y)

Tactic:
abel

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + polar f x y

Tactic:
rw [polar]

Result:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + (f (x + y) - f x - f y)
-- Mathlib/Data/Set/Basic.lean
theorem forall_in_swap {p : α → β → Prop} : (∀ a ∈ s, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ s, p a b

Proof state:
α : Type u
β : Type v
s : Set α
p : α → β → Prop
⊢ (∀ a ∈ s, ∀ (b : β), p a b) ↔ ∀ (b : β), ∀ a ∈ s, p a b

Tactic:
tauto

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma cross_mk_of_cross_ne_zero {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0)
    (h : crossProduct v w ≠ 0) :
    cross (mk F v hv) (mk F w hw) = mk F (crossProduct v w) h

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w ≠ 0
⊢ (mk F v hv).cross (mk F w hw) = mk F ((crossProduct v) w) h

Tactic:
rw [cross_mk, dif_neg h]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k)
    (p : ι → P) (b : P) :
    (s \ s₂).weightedVSubOfPoint p b w - s₂.weightedVSubOfPoint p b (-w) =
      s.weightedVSubOfPoint p b w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ((s \ s₂).weightedVSubOfPoint p b) w - (s₂.weightedVSubOfPoint p b) (-w) = (s.weightedVSubOfPoint p b) w

Tactic:
rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
lemma Finitary.sum' (h : ∀ i, (M i).Finitary) : (Matroid.sum' M).Finitary

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sum' M).Finitary

Tactic:
have := Finitary.sigma h

Result:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
this : (Matroid.sigma M).Finitary
⊢ (Matroid.sum' M).Finitary

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
this : (Matroid.sigma M).Finitary
⊢ ((Matroid.sigma M).mapEquiv (Equiv.sigmaEquivProd ι α)).Finitary

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
this : (Matroid.sigma M).Finitary
⊢ (Matroid.sum' M).Finitary

Tactic:
rw [Matroid.sum']

Result:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
this : (Matroid.sigma M).Finitary
⊢ ((Matroid.sigma M).mapEquiv (Equiv.sigmaEquivProd ι α)).Finitary