harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/ModuleCat/Free.lean
theorem linearIndependent_shortExact {w : ι' → S.X₃} (hw : LinearIndependent R w) :
    LinearIndependent R (Sum.elim (S.f ∘ v) (S.g.hom.toFun.invFun ∘ w))

Proof state:
case h.e'_4.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
x✝ : ι'
⊢ (⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w) x✝ = w x✝

Tactic:
apply Function.rightInverse_invFun ((epi_iff_surjective _).mp hS'.epi_g)

Result:
no goals

Proof state:
case h.e'_4
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ ⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w = w

Tactic:
ext

Result:
case h.e'_4.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
x✝ : ι'
⊢ (⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w) x✝ = w x✝

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R
    (⇑(ConcreteCategory.hom S.g) ∘
      Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr)

Tactic:
dsimp

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w)

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R (Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w))

Tactic:
apply linearIndependent_leftExact hS'.exact hv _ hS'.mono_f rfl

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R
    (⇑(ConcreteCategory.hom S.g) ∘
      Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr)

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w)

Tactic:
convert hw

Result:
case h.e'_4
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ ⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w = w
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem rename_esymm (n : ℕ) (e : σ ≃ τ) : rename e (esymm σ R n) = esymm τ R n :=
  calc
    rename e (esymm σ R n) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i)

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) = ∑ t ∈ powersetCard n (Finset.map e.toEmbedding univ), ∏ i ∈ t, X i

Tactic:
simp [powersetCard_map, -map_univ_equiv]

Result:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) = ∑ x ∈ powersetCard n univ, ∏ i ∈ (mapEmbedding e.toEmbedding) x, X i

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ t ∈ powersetCard n (Finset.map e.toEmbedding univ), ∏ i ∈ t, X i = ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i

Tactic:
rw [map_univ_equiv]

Result:
no goals

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ (rename ⇑e) (esymm σ R n) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i)

Tactic:
simp_rw [esymm, map_sum, map_prod, rename_X]

Result:
no goals

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) = ∑ x ∈ powersetCard n univ, ∏ i ∈ Finset.map e.toEmbedding x, X i

Tactic:
simp

Result:
no goals

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) = ∑ x ∈ powersetCard n univ, ∏ i ∈ (mapEmbedding e.toEmbedding) x, X i

Tactic:
dsimp [mapEmbedding, OrderEmbedding.ofMapLEIff]

Result:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) = ∑ x ∈ powersetCard n univ, ∏ i ∈ Finset.map e.toEmbedding x, X i
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem isReduced_reverse_iff (ω : List B) : cs.IsReduced (ω.reverse) ↔ cs.IsReduced ω

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.IsReduced ω.reverse ↔ cs.IsReduced ω

Tactic:
simp [IsReduced]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem map_comp (f : α → β) (g : β → γ) (s : WSeq α) : map (g ∘ f) s = map g (map f s)

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)

Tactic:
rw [← Seq.map_comp]

Result:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s

Proof state:
case h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) = Seq.map (Option.map g ∘ Option.map f)

Tactic:
apply congr_arg

Result:
case h.h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ map (g ∘ f) s = map g (map f s)

Tactic:
dsimp [map]

Result:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)

Proof state:
case h.h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Tactic:
ext ⟨⟩ <;> rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s

Tactic:
apply congr_fun

Result:
case h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) = Seq.map (Option.map g ∘ Option.map f)
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.inter_isBasis_iInter [Nonempty ι] {X : ι → Set α} (hI : M.Indep I)
    (h : ∀ i, M.IsBasis ((X i) ∩ I) (X i)) : M.IsBasis ((⋂ i, X i) ∩ I) (⋂ i, X i)

Proof state:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ∀ i ∈ univ, M.IsBasis ((fun i => X i.down) i ∩ I) ((fun i => X i.down) i)

Tactic:
simpa using fun (i : PLift ι) ↦ h i.down

Result:
no goals

Proof state:
case h.e'_4
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i, X i = ⋂ i, X i.down

Tactic:
exact (iInter_plift_down X).symm

Result:
no goals

Proof state:
case h.e'_4
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i, X i = ⋂ i ∈ univ, X i.down

Tactic:
simp only [mem_univ, iInter_true]

Result:
case h.e'_4
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i, X i = ⋂ i, X i.down
-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
lemma isSeparated_iff_isClosedImmersion_prod_lift {X : Scheme.{u}} :
    X.IsSeparated ↔ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))

Proof state:
case e_f
X : Scheme
⊢ pullback.diagonal (terminal.from X) = prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom

Tactic:
ext : 1 <;> simp

Result:
no goals

Proof state:
X : Scheme
⊢ autoParam (IsClosedImmersion (pullback.diagonal (terminal.from X))) _auto✝ =
    IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)

Tactic:
congr

Result:
case e_f
X : Scheme
⊢ pullback.diagonal (terminal.from X) = prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom

Proof state:
X : Scheme
⊢ X.IsSeparated ↔ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rw [isSeparated_iff, AlgebraicGeometry.isSeparated_iff, iff_iff_eq,
  ← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (prodIsoPullback X X).hom]

Result:
X : Scheme
⊢ autoParam (IsClosedImmersion (pullback.diagonal (terminal.from X))) _auto✝ =
    IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem singletonSubgraph_snd_le_subgraphOfAdj {u v : V} {h : G.Adj u v} :
    G.singletonSubgraph v ≤ G.subgraphOfAdj h

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.singletonSubgraph v ≤ G.subgraphOfAdj h

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem double_powHalf_succ_eq_powHalf (n : ℕ) : 2 * powHalf (n + 1) = powHalf n

Proof state:
n : ℕ
⊢ powHalf (n + 1) + powHalf (n + 1) = powHalf n

Tactic:
exact Quotient.sound (PGame.add_powHalf_succ_self_eq_powHalf n)

Result:
no goals

Proof state:
n : ℕ
⊢ 2 * powHalf (n + 1) = powHalf n

Tactic:
rw [two_mul]

Result:
n : ℕ
⊢ powHalf (n + 1) + powHalf (n + 1) = powHalf n
-- Mathlib/Tactic/Ring/Basic.lean
theorem atom_pf' (p : (a : R) = a') :
    a = a' ^ (nat_lit 1).rawCast * (nat_lit 1).rawCast + 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a a' : R
p : a = a'
⊢ a = a' ^ Nat.rawCast 1 * Nat.rawCast 1 + 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_injective_right (a : α) : Injective fun b => [[b, a]] := fun b c h => by
  rw [Finset.ext_iff] at h
  exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Proof state:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : ∀ (a_1 : α), a_1 ∈ (fun b => [[b, a]]) b ↔ a_1 ∈ (fun b => [[b, a]]) c
⊢ b = c

Tactic:
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c
⊢ b = c

Tactic:
rw [Finset.ext_iff] at h

Result:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : ∀ (a_1 : α), a_1 ∈ (fun b => [[b, a]]) b ↔ a_1 ∈ (fun b => [[b, a]]) c
⊢ b = c
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem eq_lift_inv_left {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
    f = lift (g ≫ B.inv) h ≫ B.mul ↔ lift g f ≫ B.mul = h

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g h : A ⟶ B.X
⊢ lift g f ≫ B.mul = h → f = lift (g ≫ B.inv) h ≫ B.mul

Tactic:
rintro rfl

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g : A ⟶ B.X
⊢ f = lift (g ≫ B.inv) (lift g f ≫ B.mul) ≫ B.mul

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g : A ⟶ B.X
⊢ f = lift (g ≫ B.inv) (lift g f ≫ B.mul) ≫ B.mul

Tactic:
simp [← lift_lift_assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g h : A ⟶ B.X
⊢ f = lift (g ≫ B.inv) h ≫ B.mul ↔ lift g f ≫ B.mul = h

Tactic:
refine ⟨?_, ?_⟩ <;> (rintro rfl; simp [← lift_lift_assoc])

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsVanKampenColimit.of_iso {F : J ⥤ C} {c c' : Cocone F} (H : IsVanKampenColimit c)
    (e : c ≅ c') : IsVanKampenColimit c'

Proof state:
case h
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this✝ : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι
j : J
this : IsIso e.inv.hom
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j) ↔
    IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)

Tactic:
exact (IsPullback.of_vert_isIso ⟨by simp⟩).paste_vert_iff (NatTrans.congr_app h j).symm

Result:
no goals

Proof state:
case h
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι
⊢ ∀ (a : J),
    IsPullback (c''.ι.app a) (α.app a) (f ≫ e.inv.hom) (c.ι.app a) ↔ IsPullback (c''.ι.app a) (α.app a) f (c'.ι.app a)

Tactic:
intro j

Result:
case h
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem adjoin_simple_toSubalgebra_of_integral (hα : IsIntegral F α) :
    F⟮α⟯.toSubalgebra = Algebra.adjoin F {α}

Proof state:
case hS
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
hα : IsIntegral F α
⊢ ∀ x ∈ {α}, IsAlgebraic F x

Tactic:
rintro x (rfl : x = α)

Result:
case hS
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hα : IsIntegral F x
⊢ IsAlgebraic F x

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
hα : IsIntegral F α
⊢ F⟮α⟯.toSubalgebra = Algebra.adjoin F {α}

Tactic:
apply adjoin_algebraic_toSubalgebra

Result:
case hS
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
hα : IsIntegral F α
⊢ ∀ x ∈ {α}, IsAlgebraic F x

Proof state:
case hS
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hα : IsIntegral F x
⊢ IsAlgebraic F x

Tactic:
rwa [isAlgebraic_iff_isIntegral]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_mono {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f g : α →₁[μ] G'}
    (hfg : f ≤ g) : setToL1 hT f ≤ setToL1 hT g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(Lp G' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ (setToL1 hT) g - (setToL1 hT) f

Tactic:
rw [← (setToL1 hT).map_sub]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(Lp G' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ (setToL1 hT) (g - f)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(Lp G' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ (setToL1 hT) (g - f)

Tactic:
exact setToL1_nonneg hT hT_nonneg hfg

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(Lp G' 1 μ)
hfg : f ≤ g
⊢ (setToL1 hT) f ≤ (setToL1 hT) g

Tactic:
rw [← sub_nonneg] at hfg ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(Lp G' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ (setToL1 hT) g - (setToL1 hT) f
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma rightHomologyMap_nullHomotopic [S₁.HasRightHomology] [S₂.HasRightHomology]
    (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : h₀ ≫ S₂.f = 0)
    (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : S₁.g ≫ h₃ = 0) :
    rightHomologyMap (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Tactic:
apply rightHomologyMap'_nullHomotopic

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem inv [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : M⁻¹.PosDef

Proof state:
case refine_3
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
this : 0 < star (M⁻¹ *ᵥ x) ⬝ᵥ M *ᵥ M⁻¹ *ᵥ x
_inst : Invertible M := ⋯.invertible
⊢ 0 < star x ⬝ᵥ M⁻¹ *ᵥ x

Tactic:
rwa [star_mulVec, mulVec_mulVec, Matrix.mul_inv_of_invertible, one_mulVec,
  ← star_pos_iff, ← star_mulVec, ← star_dotProduct] at this

Result:
no goals

Proof state:
case refine_1
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ IsUnit M⁻¹

Tactic:
simpa using hM.isUnit

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M⁻¹ *ᵥ x

Tactic:
have := hM.2 (M⁻¹ *ᵥ x) ((Matrix.mulVec_injective_iff_isUnit.mpr ?_ |>.ne_iff' ?_).2 hx)

Result:
case refine_3
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
this : 0 < star (M⁻¹ *ᵥ x) ⬝ᵥ M *ᵥ M⁻¹ *ᵥ x
⊢ 0 < star x ⬝ᵥ M⁻¹ *ᵥ x

case refine_1
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ IsUnit M⁻¹

case refine_2
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ M⁻¹ *ᵥ 0 = 0

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ M⁻¹.PosDef

Tactic:
refine ⟨hM.isHermitian.inv, fun x hx => ?_⟩

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M⁻¹ *ᵥ x

Proof state:
case refine_3
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
this : 0 < star (M⁻¹ *ᵥ x) ⬝ᵥ M *ᵥ M⁻¹ *ᵥ x
⊢ 0 < star x ⬝ᵥ M⁻¹ *ᵥ x

Tactic:
let _inst := hM.isUnit.invertible

Result:
case refine_3
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
this : 0 < star (M⁻¹ *ᵥ x) ⬝ᵥ M *ᵥ M⁻¹ *ᵥ x
_inst : Invertible M := ⋯.invertible
⊢ 0 < star x ⬝ᵥ M⁻¹ *ᵥ x

Proof state:
case refine_2
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ M⁻¹ *ᵥ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_concat (x : BitVec w) (b : Bool) :
    (concat x b).toInt = if w = 0 then -b.toInt else x.toInt * 2 + b.toInt

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ (if 2 * (x.toNat * 2 + b.toNat) < 2 ^ (w + 1) then ↑(x.toNat * 2 + b.toNat)
    else ↑(x.toNat * 2 + b.toNat) - ↑(2 ^ (w + 1))) =
    if w = 0 then -b.toInt else (if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) * 2 + b.toInt

Tactic:
cases w

Result:
case zero
b : Bool
x : BitVec 0
⊢ (if 2 * (x.toNat * 2 + b.toNat) < 2 ^ (0 + 1) then ↑(x.toNat * 2 + b.toNat)
    else ↑(x.toNat * 2 + b.toNat) - ↑(2 ^ (0 + 1))) =
    if 0 = 0 then -b.toInt else (if 2 * x.toNat < 2 ^ 0 then ↑x.toNat else ↑x.toNat - ↑(2 ^ 0)) * 2 + b.toInt

case succ
b : Bool
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (if 2 * (x.toNat * 2 + b.toNat) < 2 ^ (n✝ + 1 + 1) then ↑(x.toNat * 2 + b.toNat)
    else ↑(x.toNat * 2 + b.toNat) - ↑(2 ^ (n✝ + 1 + 1))) =
    if n✝ + 1 = 0 then -b.toInt
    else (if 2 * x.toNat < 2 ^ (n✝ + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (n✝ + 1))) * 2 + b.toInt

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ (x.concat b).toInt = if w = 0 then -b.toInt else x.toInt * 2 + b.toInt

Tactic:
simp only [BitVec.toInt, toNat_concat]

Result:
w : Nat
x : BitVec w
b : Bool
⊢ (if 2 * (x.toNat * 2 + b.toNat) < 2 ^ (w + 1) then ↑(x.toNat * 2 + b.toNat)
    else ↑(x.toNat * 2 + b.toNat) - ↑(2 ^ (w + 1))) =
    if w = 0 then -b.toInt else (if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) * 2 + b.toInt

Proof state:
case zero
b : Bool
x : BitVec 0
⊢ (if 2 * (x.toNat * 2 + b.toNat) < 2 ^ (0 + 1) then ↑(x.toNat * 2 + b.toNat)
    else ↑(x.toNat * 2 + b.toNat) - ↑(2 ^ (0 + 1))) =
    if 0 = 0 then -b.toInt else (if 2 * x.toNat < 2 ^ 0 then ↑x.toNat else ↑x.toNat - ↑(2 ^ 0)) * 2 + b.toInt

Tactic:
cases b <;> simp [eq_nil x]

Result:
no goals

Proof state:
case succ
b : Bool
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (if 2 * (x.toNat * 2 + b.toNat) < 2 ^ (n✝ + 1 + 1) then ↑(x.toNat * 2 + b.toNat)
    else ↑(x.toNat * 2 + b.toNat) - ↑(2 ^ (n✝ + 1 + 1))) =
    if n✝ + 1 = 0 then -b.toInt
    else (if 2 * x.toNat < 2 ^ (n✝ + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (n✝ + 1))) * 2 + b.toInt

Tactic:
cases b <;> simp <;> omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isEmpty_eq_true {l : Array α} : l.isEmpty ↔ l = #[]

Proof state:
α : Type u_1
l : Array α
⊢ l.isEmpty = true ↔ l = #[]

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem Irreducible.gcd_eq_one_iff [NormalizedGCDMonoid α] {x y : α} (hx : Irreducible x) :
    gcd x y = 1 ↔ ¬(x ∣ y)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ ¬x ∣ y

Tactic:
rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]

Result:
no goals