harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_iff_comp_left (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : QuasiIso φ] :
    QuasiIso (φ ≫ φ') ↔ QuasiIso φ'

Proof state:
case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
a✝ : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ')

Tactic:
exact quasiIso_comp φ φ'

Result:
no goals

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ'

Tactic:
constructor

Result:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ') → QuasiIso φ'

case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso φ' → QuasiIso (φ ≫ φ')

Proof state:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ') → QuasiIso φ'

Tactic:
intro

Result:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
a✝ : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'

Proof state:
case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso φ' → QuasiIso (φ ≫ φ')

Tactic:
intro

Result:
case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
a✝ : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ')

Proof state:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
a✝ : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'

Tactic:
exact quasiIso_of_comp_left φ φ'

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem IsConnected.union {s t : Set α} (H : (s ∩ t).Nonempty) (Hs : IsConnected s)
    (Ht : IsConnected t) : IsConnected (s ∪ t)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
Hs : IsConnected s
Ht : IsConnected t
⊢ IsConnected (s ∪ t)

Tactic:
rcases H with ⟨x, hx⟩

Result:
case intro
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)

Proof state:
case intro
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)

Tactic:
refine ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩

Result:
case intro
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)

Proof state:
case intro
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)

Tactic:
exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx)
  Ht.isPreconnected

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_eq_stopping_time [AddGroup ι] [TopologicalSpace ι] [MeasurableSpace ι]
    [BorelSpace ι] [OrderTopology ι] [MeasurableSingletonClass ι] [SecondCountableTopology ι]
    [MeasurableSub₂ ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω = π ω}

Proof state:
case h.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω = π ω ∧ τ ω ≤ j
⊢ π ω ≤ j

Tactic:
rw [← h.1]

Result:
case h.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω = π ω ∧ τ ω ≤ j
⊢ τ ω ≤ j
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem atEnd_of_valid (cs : List Char) (cs' : List Char) :
    atEnd ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ ↔ cs' = []

Proof state:
cs cs' : List Char
⊢ { data := cs ++ cs' }.atEnd { byteIdx := utf8Len cs } = true ↔ cs' = []

Tactic:
rw [atEnd_iff]

Result:
cs cs' : List Char
⊢ { data := cs ++ cs' }.endPos ≤ { byteIdx := utf8Len cs } ↔ cs' = []

Proof state:
cs cs' : List Char
⊢ { data := cs ++ cs' }.endPos ≤ { byteIdx := utf8Len cs } ↔ cs' = []

Tactic:
cases cs' <;> simp [add_utf8Size_pos]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma leftHomology_ext_iff {A : C} (f₁ f₂ : S.leftHomology ⟶ A) :
    f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
f₁ f₂ : S.leftHomology ⟶ A
⊢ f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂

Tactic:
rw [cancel_epi]

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem bernoulliFun_eval_one (k : ℕ) : bernoulliFun k 1 = bernoulliFun k 0 + ite (k = 1) 1 0

Proof state:
case pos
k : ℕ
h : k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 1

Tactic:
rw [h, bernoulli_one, bernoulli'_one, eq_ratCast]

Result:
case pos
k : ℕ
h : k = 1
⊢ ↑(1 / 2) = ↑(-1 / 2) + 1

Proof state:
k : ℕ
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + if k = 1 then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
k : ℕ
h : k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 1

case neg
k : ℕ
h : ¬k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 0

Proof state:
k : ℕ
⊢ bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0

Tactic:
rw [bernoulliFun, bernoulliFun_eval_zero, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one]

Result:
k : ℕ
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + if k = 1 then 1 else 0

Proof state:
case pos
k : ℕ
h : k = 1
⊢ 1 / 2 = -1 / 2 + 1

Tactic:
ring

Result:
no goals

Proof state:
case neg
k : ℕ
h : ¬k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 0

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one h, add_zero, eq_ratCast]

Result:
no goals

Proof state:
case pos
k : ℕ
h : k = 1
⊢ ↑(1 / 2) = ↑(-1 / 2) + 1

Tactic:
push_cast

Result:
case pos
k : ℕ
h : k = 1
⊢ 1 / 2 = -1 / 2 + 1
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖x‖ / Real.Angle.cos (o.oangle x (x + y)) = ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
@[reassoc (attr := simp)]
lemma rightDerivedNatTrans_fac (τ : F ⟶ F') :
    α ≫ whiskerLeft L (rightDerivedNatTrans RF RF' α α' W τ) = τ ≫ α'

Proof state:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_6} D
inst✝² : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
⊢ α ≫ whiskerLeft L (RF.rightDerivedNatTrans RF' α α' W τ) = τ ≫ α'

Tactic:
dsimp only [rightDerivedNatTrans]

Result:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_6} D
inst✝² : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
⊢ α ≫ whiskerLeft L (RF.rightDerivedDesc α W RF' (τ ≫ α')) = τ ≫ α'

Proof state:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_6} D
inst✝² : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
⊢ α ≫ whiskerLeft L (RF.rightDerivedDesc α W RF' (τ ≫ α')) = τ ≫ α'

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_image_embedding (f : α ↪ β) (s : Set α) : #(f '' s) = #s

Proof state:
α β : Type u
f : α ↪ β
s : Set α
⊢ #↑(⇑f '' s) = #↑s

Tactic:
simpa using mk_image_embedding_lift f s

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem closure_Ioi' {a : α} (h : (Ioi a).Nonempty) : closure (Ioi a) = Ici a

Proof state:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure (Ioi a)

Tactic:
rw [← diff_subset_closure_iff, Ici_diff_Ioi_same, singleton_subset_iff]

Result:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ a ∈ closure (Ioi a)

Proof state:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ a ∈ closure (Ioi a)

Tactic:
exact isGLB_Ioi.mem_closure h

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ closure (Ioi a) ⊆ Ici a

Tactic:
exact closure_minimal Ioi_subset_Ici_self isClosed_Ici

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ closure (Ioi a) = Ici a

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ closure (Ioi a) ⊆ Ici a

case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure (Ioi a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
    (o.map f).get h = f (o.get (by simpa using h))

Proof state:
α : Type ?u.16435
β : Type ?u.16438
f : α → β
o : Option α
h : (Option.map f o).isSome = true
⊢ o.isSome = true

Tactic:
simpa using h

Result:
no goals

Proof state:
case none
α : Type u_1
β : Type u_2
f : α → β
h : (Option.map f none).isSome = true
⊢ (Option.map f none).get h = f (none.get ⋯)

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
o : Option α
h : (Option.map f o).isSome = true
⊢ (Option.map f o).get h = f (o.get ⋯)

Tactic:
cases o with
| none => simp at h
| some a => simp

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
f : α → β
a : α
h : (Option.map f (some a)).isSome = true
⊢ (Option.map f (some a)).get h = f ((some a).get ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
/-- Every element of `⨂[R] i, s i` has a lift in `FreeAddMonoid (R × Π i, s i)`.
-/
lemma nonempty_lifts (x : ⨂[R] i, s i) : Set.Nonempty (lifts x)

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ x.lifts.Nonempty

Tactic:
existsi @Quotient.out _ (addConGen (PiTensorProduct.Eqv R s)).toSetoid x

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ Quotient.out x ∈ x.lifts

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ ↑(Quotient.out x) = x

Tactic:
rw [← AddCon.quot_mk_eq_coe]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ Quot.mk (⇑(addConGen (Eqv R s))) (Quotient.out x) = x

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ Quotient.out x ∈ x.lifts

Tactic:
simp only [lifts, Set.mem_setOf_eq]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ ↑(Quotient.out x) = x

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ Quot.mk (⇑(addConGen (Eqv R s))) (Quotient.out x) = x

Tactic:
erw [Quot.out_eq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_neg_orientation_eq_neg (x y : V) : (-o).oangle x y = -o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (-o).oangle x y = -o.oangle x y

Tactic:
simp [oangle]

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
/-- In `Fin n`, all elements are odd for odd `n`,
otherwise an element is odd iff its `Fin.val` value is odd. -/
lemma odd_iff {n : ℕ} [NeZero n] {k : Fin n} : Odd k ↔ Odd n ∨ Odd k.val

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
hk : Odd k
⊢ Odd n ∨ Odd ↑k

Tactic:
rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]

Result:
n : ℕ
inst✝ : NeZero n
k : Fin n
hk : Odd k
⊢ Even n → Odd ↑k

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
hk : Odd k
⊢ Even n → Odd ↑k

Tactic:
exact fun hn ↦ (odd_iff_of_even hn).mp hk

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Gershgorin.lean
theorem det_ne_zero_of_sum_col_lt_diag (h : ∀ k, ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖) :
    A.det ≠ 0

Proof state:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A.transpose k j‖ < ‖A.transpose k k‖

Tactic:
simp_rw [Matrix.transpose_apply]

Result:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ x ∈ Finset.univ.erase k, ‖A x k‖ < ‖A k k‖

Proof state:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ x ∈ Finset.univ.erase k, ‖A x k‖ < ‖A k k‖

Tactic:
exact h

Result:
no goals

Proof state:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.det ≠ 0

Tactic:
rw [← Matrix.det_transpose]

Result:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.transpose.det ≠ 0

Proof state:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.transpose.det ≠ 0

Tactic:
exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ioc : (some : α → WithBot α) '' Ioc a b = Ioc (a : WithBot α) b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b

Tactic:
rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2]
    (f1 : σ1) (f2 : σ2) :
    Unsatisfiable α f1 → Incompatible α f1 f2

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Unsatisfiable α f1
a : α → Bool
⊢ ¬(a ⊨ f1) ∨ ¬(a ⊨ f2)

Tactic:
exact Or.inl <| h a

Result:
no goals

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Unsatisfiable α f1 → Incompatible α f1 f2

Tactic:
intro h a

Result:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Unsatisfiable α f1
a : α → Bool
⊢ ¬(a ⊨ f1) ∨ ¬(a ⊨ f2)
-- Mathlib/Algebra/QuadraticDiscriminant.lean
lemma discrim_lt_zero_of_neg (ha : a ≠ 0) (h : ∀ x : K, a * (x * x) + b * x + c < 0) :
    discrim a b c < 0 :=
  discrim_neg a b c ▸ discrim_lt_zero (neg_ne_zero.2 ha) <| by
    simpa only [neg_mul, ← neg_add, neg_pos]

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), a * (x * x) + b * x + c < 0
⊢ ∀ (x : K), 0 < -a * (x * x) + -b * x + -c

Tactic:
simpa only [neg_mul, ← neg_add, neg_pos]

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem IsConnected.of_induct {j₀ : J}
    (h : ∀ p : Set J, j₀ ∈ p → (∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ j : J, j ∈ p) :
    IsConnected J :=
  have := Nonempty.intro j₀
  IsConnected.of_constant_of_preserves_morphisms fun {α} F a => by
    have w := h { j | F j = F j₀ } rfl (fun {j₁} {j₂} f => by
      change F j₁ = F j₀ ↔ F j₂ = F j₀
      simp [a f])
    intro j j'
    rw [w j, w j']

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
j j' : J
⊢ F j = F j'

Tactic:
rw [w j, w j']

Result:
no goals

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'

Tactic:
intro j j'

Result:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
j j' : J
⊢ F j = F j'

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F j₁ = F j₀ ↔ F j₂ = F j₀

Tactic:
simp [a f]

Result:
no goals

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
⊢ ∀ (j j' : J), F j = F j'

Tactic:
have w := h { j | F j = F j₀ } rfl (fun {j₁} {j₂} f => by
  change F j₁ = F j₀ ↔ F j₂ = F j₀
  simp [a f])

Result:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ j₁ ∈ {j | F j = F j₀} ↔ j₂ ∈ {j | F j = F j₀}

Tactic:
change F j₁ = F j₀ ↔ F j₂ = F j₀

Result:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F j₁ = F j₀ ↔ F j₂ = F j₀