harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/CoverPreserving.lean
theorem CompatiblePreserving.apply_map {Y : C} {f : Y ⟶ Z} (hf : T f) :
    x.functorPushforward G (G.map f) (image_mem_functorPushforward G T hf) = x f hf

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ f' ≫ G.map g = 𝟙 (G.obj Y) ≫ G.map f

Tactic:
simp [eq]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
⊢ FamilyOfElements.functorPushforward G x (G.map f) ⋯ = x f hf

Tactic:
unfold FamilyOfElements.functorPushforward

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
⊢ (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure ⋯) fun Z_1 g h h₁ fac =>
      ℱ.val.map h.op (x g h₁)) =
    x f hf

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
⊢ (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure ⋯) fun Z_1 g h h₁ fac =>
      ℱ.val.map h.op (x g h₁)) =
    x f hf

Tactic:
rcases getFunctorPushforwardStructure (image_mem_functorPushforward G T hf) with
  ⟨X, g, f', hg, eq⟩

Result:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ (FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf

Proof state:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ (FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf

Tactic:
simpa using hG.compatible ℱ h f' (𝟙 _) hg hf (by simp [eq])

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem not_commute_of_disjoint_movedBy_preimage {g h : G} (ne_one : g ≠ 1)
    (disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)) : ¬Commute g h

Proof state:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
ne_one : g ≠ 1
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
⊢ ¬Commute g h

Tactic:
contrapose! ne_one with comm

Result:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
⊢ g = 1

Proof state:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
⊢ g = 1

Tactic:
rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
  compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem pair_eq_singleton_iff {x y z : ZFSet} : ({x, y} : ZFSet) = {z} ↔ x = z ∧ y = z

Proof state:
case refine_2
x y z : ZFSet.{u_1}
⊢ x = z ∧ y = z → {x, y} = {z}

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case refine_2.intro
y : ZFSet.{u_1}
⊢ {y, y} = {y}

Proof state:
case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x ∈ {z} ∧ y ∈ {z}

Tactic:
simp [← h]

Result:
no goals

Proof state:
x y z : ZFSet.{u_1}
⊢ {x, y} = {z} ↔ x = z ∧ y = z

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x = z ∧ y = z

case refine_2
x y z : ZFSet.{u_1}
⊢ x = z ∧ y = z → {x, y} = {z}

Proof state:
case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x = z ∧ y = z

Tactic:
rw [← mem_singleton, ← mem_singleton]

Result:
case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x ∈ {z} ∧ y ∈ {z}

Proof state:
case refine_2.intro
y : ZFSet.{u_1}
⊢ {y, y} = {y}

Tactic:
exact pair_eq_singleton y

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma _root_.Commute.sum_right (s : Finset ι) (f : ι → α) (b : α)
    (h : ∀ i ∈ s, Commute b (f i)) : Commute b (∑ i ∈ s, f i) :=
  (Commute.multiset_sum_right _ _) fun b hb => by
    obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hb
    exact h _ hi

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : NonUnitalNonAssocSemiring α
s : Finset ι
f : ι → α
b✝ : α
h : ∀ i ∈ s, Commute b✝ (f i)
b : α
hb : b ∈ Multiset.map (fun i => f i) s.val
⊢ Commute b✝ b

Tactic:
obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hb

Result:
case intro.intro
ι : Type u_1
α : Type u_3
inst✝ : NonUnitalNonAssocSemiring α
s : Finset ι
f : ι → α
b : α
h : ∀ i ∈ s, Commute b (f i)
i : ι
hi : i ∈ s.val
hb : f i ∈ Multiset.map (fun i => f i) s.val
⊢ Commute b (f i)

Proof state:
case intro.intro
ι : Type u_1
α : Type u_3
inst✝ : NonUnitalNonAssocSemiring α
s : Finset ι
f : ι → α
b : α
h : ∀ i ∈ s, Commute b (f i)
i : ι
hi : i ∈ s.val
hb : f i ∈ Multiset.map (fun i => f i) s.val
⊢ Commute b (f i)

Tactic:
exact h _ hi

Result:
no goals
-- Mathlib/CategoryTheory/Monad/Algebra.lean
theorem coalgebra_iso_of_iso {A B : Coalgebra G} (f : A ⟶ B) [IsIso f.f] : IsIso f :=
  ⟨⟨{   f := inv f.f
        h

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A ∧ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 B

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ A.a ≫ G.map f.f ≫ G.map (inv f.f) = A.a

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a

Tactic:
rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ A.a ≫ G.map f.f ≫ G.map (inv f.f) = A.a
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma natDegree_eq_of_natDegree_add_eq_zero (p q : R[X])
    (H : natDegree (p + q) = 0) : natDegree p = natDegree q

Proof state:
case neg.H
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ (p + q).natDegree < q.natDegree

Tactic:
rwa [H, Nat.pos_iff_ne_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
by_cases h₁ : natDegree p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
exact h₁.trans h₂.symm

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
by_cases h₂ : natDegree q = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree

Proof state:
case neg.H
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ (p + q).natDegree < p.natDegree

Tactic:
rwa [H, Nat.pos_iff_ne_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
apply natDegree_eq_of_natDegree_add_lt_right

Result:
case neg.H
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ (p + q).natDegree < q.natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
apply natDegree_eq_of_natDegree_add_lt_left

Result:
case neg.H
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ (p + q).natDegree < p.natDegree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
on_goal 1 => by_cases h₂ : natDegree q = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
/-- `SL(2, ℤ)` is generated by `S` and `T`. -/
lemma SpecialLinearGroup.SL2Z_generators : closure {S, T} = ⊤

Proof state:
case hT
B : FixedDetMatrix (Fin 2) ℤ 1
hb : B ∈ closure {S, T}
⊢ T • B ∈ closure {S, T}

Tactic:
exact mul_mem (subset_closure (Set.mem_insert_of_mem S rfl)) hb

Result:
no goals

Proof state:
case h0
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a✝ : 0 ≤ ↑A 0 1
a6 : |↑A 0 1| < |↑A 1 1|
⊢ A ∈ closure {S, T}

Tactic:
rw [reps_one_id A a1 a4 a6]

Result:
case h0
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a✝ : 0 ≤ ↑A 0 1
a6 : |↑A 0 1| < |↑A 1 1|
⊢ 1 ∈ closure {S, T}

Proof state:
case h0
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a✝ : 0 ≤ ↑A 0 1
a6 : |↑A 0 1| < |↑A 1 1|
⊢ 1 ∈ closure {S, T}

Tactic:
exact one_mem _

Result:
no goals

Proof state:
case hS
B : FixedDetMatrix (Fin 2) ℤ 1
hb : B ∈ closure {S, T}
⊢ S • B ∈ closure {S, T}

Tactic:
exact mul_mem (subset_closure (Set.mem_insert S {T})) hb

Result:
no goals

Proof state:
⊢ ∀ (x : SL(2, ℤ)), x ∈ closure {S, T}

Tactic:
intro A

Result:
A : SL(2, ℤ)
⊢ A ∈ closure {S, T}

Proof state:
⊢ closure {S, T} = ⊤

Tactic:
rw [eq_top_iff']

Result:
⊢ ∀ (x : SL(2, ℤ)), x ∈ closure {S, T}

Proof state:
A : SL(2, ℤ)
⊢ A ∈ closure {S, T}

Tactic:
induction A using (induction_on one_ne_zero) with
| h0 A a1 a4 _ a6 =>
  rw [reps_one_id A a1 a4 a6]
  exact one_mem _
| hS B hb =>
  exact mul_mem (subset_closure (Set.mem_insert S {T})) hb
| hT B hb =>
  exact mul_mem (subset_closure (Set.mem_insert_of_mem S rfl)) hb

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
theorem Prepartition.measure_iUnion_toReal [Finite ι] {I : Box ι} (π : Prepartition I)
    (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] :
    (μ π.iUnion).toReal = ∑ J ∈ π.boxes, (μ J).toReal

Proof state:
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ (μ π.iUnion).toReal = ∑ J ∈ π.boxes, (μ ↑J).toReal

Tactic:
erw [← ENNReal.toReal_sum, π.iUnion_def, measure_biUnion_finset π.pairwiseDisjoint]

Result:
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ b ∈ π.boxes, MeasurableSet ↑b

ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ a ∈ π.boxes, μ ↑a ≠ ⊤

Proof state:
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ b ∈ π.boxes, MeasurableSet ↑b

ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ a ∈ π.boxes, μ ↑a ≠ ⊤

Tactic:
exacts [fun J _ => J.measurableSet_coe, fun J _ => (J.measure_coe_lt_top μ).ne]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap_comp (hom : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) :
    nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j => hom i j ≫ g.f j

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
n : ι
⊢ (C.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ D.dTo n) ≫ g.f n =
    C.dFrom n ≫ hom (c.next n) n ≫ g.f n + (hom n (c.prev n) ≫ g.f (c.prev n)) ≫ E.dTo n

Tactic:
simp only [Preadditive.add_comp, assoc, g.comm]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
⊢ nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j => hom i j ≫ g.f j

Tactic:
ext n

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
n : ι
⊢ (nullHomotopicMap hom ≫ g).f n = (nullHomotopicMap fun i j => hom i j ≫ g.f j).f n

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
n : ι
⊢ (nullHomotopicMap hom ≫ g).f n = (nullHomotopicMap fun i j => hom i j ≫ g.f j).f n

Tactic:
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
n : ι
⊢ (C.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ D.dTo n) ≫ g.f n =
    C.dFrom n ≫ hom (c.next n) n ≫ g.f n + (hom n (c.prev n) ≫ g.f (c.prev n)) ≫ E.dTo n
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
lemma aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix :
    P.aevalDifferential.toMatrix' = (aeval P.val).mapMatrix P.jacobiMatrix

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ LinearMap.toMatrix' P.aevalDifferential i j = (aeval P.val).mapMatrix P.jacobiMatrix i j

Tactic:
rw [← LinearMap.toMatrix_eq_toMatrix']

Result:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (LinearMap.toMatrix (Pi.basisFun S P.rels) (Pi.basisFun S P.rels)) P.aevalDifferential i j =
    (aeval P.val).mapMatrix P.jacobiMatrix i j

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ ((Pi.basisFun S P.rels).repr (P.aevalDifferential ((Pi.basisFun S P.rels) j))) i =
    (aeval P.val).mapMatrix P.jacobiMatrix i j

Tactic:
simp [jacobiMatrix_apply]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
⊢ LinearMap.toMatrix' P.aevalDifferential = (aeval P.val).mapMatrix P.jacobiMatrix

Tactic:
ext i j : 1

Result:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ LinearMap.toMatrix' P.aevalDifferential i j = (aeval P.val).mapMatrix P.jacobiMatrix i j

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (LinearMap.toMatrix (Pi.basisFun S P.rels) (Pi.basisFun S P.rels)) P.aevalDifferential i j =
    (aeval P.val).mapMatrix P.jacobiMatrix i j

Tactic:
rw [LinearMap.toMatrix_apply]

Result:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ ((Pi.basisFun S P.rels).repr (P.aevalDifferential ((Pi.basisFun S P.rels) j))) i =
    (aeval P.val).mapMatrix P.jacobiMatrix i j
-- Mathlib/Algebra/Module/Defs.lean
theorem two_smul : (2 : R) • x = x + x

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ 2 • x = x + x

Tactic:
rw [← one_add_one_eq_two, add_smul, one_smul]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem ext_iff {p q : SkewMonoidAlgebra k G} : p = q ↔ ∀ n, coeff p n = coeff q n

Proof state:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f g : G →₀ k
⊢ { toFinsupp := f } = { toFinsupp := g } ↔ ∀ (n : G), { toFinsupp := f }.coeff n = { toFinsupp := g }.coeff n

Tactic:
simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p q : SkewMonoidAlgebra k G
⊢ p = q ↔ ∀ (n : G), p.coeff n = q.coeff n

Tactic:
rcases p with ⟨f : G →₀ k⟩

Result:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
q : SkewMonoidAlgebra k G
f : G →₀ k
⊢ { toFinsupp := f } = q ↔ ∀ (n : G), { toFinsupp := f }.coeff n = q.coeff n

Proof state:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
q : SkewMonoidAlgebra k G
f : G →₀ k
⊢ { toFinsupp := f } = q ↔ ∀ (n : G), { toFinsupp := f }.coeff n = q.coeff n

Tactic:
rcases q with ⟨g : G →₀ k⟩

Result:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f g : G →₀ k
⊢ { toFinsupp := f } = { toFinsupp := g } ↔ ∀ (n : G), { toFinsupp := f }.coeff n = { toFinsupp := g }.coeff n
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem isAdjointPair_inner (A : E →ₗ[𝕜] F) :
    IsAdjointPair (sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜) (sesqFormOfInner : F →ₗ[𝕜] F →ₗ⋆[𝕜] 𝕜) A
      (LinearMap.adjoint A)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
⊢ (sesqFormOfInner (A x)) y = (sesqFormOfInner x) ((adjoint A) y)

Tactic:
simp only [sesqFormOfInner_apply_apply, adjoint_inner_left]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ sesqFormOfInner.IsAdjointPair sesqFormOfInner ⇑A ⇑(adjoint A)

Tactic:
intro x y

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
⊢ (sesqFormOfInner (A x)) y = (sesqFormOfInner x) ((adjoint A) y)
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_shiftLeft (m : Num) (n : Nat) : ↑(m <<< n) = (m : ℕ) <<< (n : ℕ)

Proof state:
case pos.zero
a✝ : PosNum
⊢ ↑(a✝ <<< 0) = ↑a✝ <<< 0

Tactic:
rfl

Result:
no goals

Proof state:
case zero
n : ℕ
⊢ ↑0 = ↑zero <<< n

Tactic:
symm

Result:
case zero
n : ℕ
⊢ ↑zero <<< n = ↑0

Proof state:
case pos.succ
a✝ : PosNum
n : ℕ
IH : ↑(a✝ <<< n) = ↑a✝ <<< n
⊢ ↑(a✝ <<< (n + 1)) = ↑a✝ <<< (n + 1)

Tactic:
simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftLeft_succ, IH, pow_succ, ← mul_assoc, mul_comm,
      -shiftl_eq_shiftLeft, -PosNum.shiftl_eq_shiftLeft, shiftl, mul_two]

Result:
no goals

Proof state:
m : Num
n : ℕ
⊢ ↑(m <<< n) = ↑m <<< n

Tactic:
cases m <;> dsimp only [← shiftl_eq_shiftLeft, shiftl]

Result:
case zero
n : ℕ
⊢ ↑0 = ↑zero <<< n

case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos (a✝ <<< n)) = ↑(pos a✝) <<< n

Proof state:
case pos
n : ℕ
a✝ : PosNum
⊢ ↑(a✝ <<< n) = ↑a✝ <<< n

Tactic:
induction' n with n IH

Result:
case pos.zero
a✝ : PosNum
⊢ ↑(a✝ <<< 0) = ↑a✝ <<< 0

case pos.succ
a✝ : PosNum
n : ℕ
IH : ↑(a✝ <<< n) = ↑a✝ <<< n
⊢ ↑(a✝ <<< (n + 1)) = ↑a✝ <<< (n + 1)

Proof state:
case zero
n : ℕ
⊢ ↑zero <<< n = ↑0

Tactic:
apply Nat.zero_shiftLeft

Result:
no goals

Proof state:
case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos (a✝ <<< n)) = ↑(pos a✝) <<< n

Tactic:
simp only [cast_pos]

Result:
case pos
n : ℕ
a✝ : PosNum
⊢ ↑(a✝ <<< n) = ↑a✝ <<< n
-- Mathlib/Analysis/Normed/Group/Seminorm.lean
theorem smul_sup (r : R) (p q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
  have Real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => Real.smul_max _ _

Proof state:
R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : NonarchAddGroupSeminorm E
x y : ℝ
⊢ r • (x ⊔ y) = r • x ⊔ r • y

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem Adapted.integrable_upcrossingsBefore [IsFiniteMeasure μ] (hf : Adapted ℱ f) (hab : a < b) :
    Integrable (fun ω => (upcrossingsBefore a b f N ω : ℝ)) μ :=
  haveI : ∀ᵐ ω ∂μ, ‖(upcrossingsBefore a b f N ω : ℝ)‖ ≤ N

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ ‖↑(upcrossingsBefore a b f N ω)‖ ≤ ↑N

Tactic:
rw [Real.norm_eq_abs, Nat.abs_cast, Nat.cast_le]

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω ≤ N

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
⊢ ∀ᵐ (ω : Ω) ∂μ, ‖↑(upcrossingsBefore a b f N ω)‖ ≤ ↑N

Tactic:
filter_upwards with ω

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ ‖↑(upcrossingsBefore a b f N ω)‖ ≤ ↑N

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
exact upcrossingsBefore_le _ _ hab

Result:
no goals
-- Mathlib/Order/Fin/Basic.lean
theorem succ_top (n : ℕ) [NeZero n] : (⊤ : Fin n).succ = ⊤

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ⊤.succ = ⊤

Tactic:
rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']

Result:
no goals