harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem ι_eq_v_add_smul_e0 (m : M) (r : R) : ι (Q' Q) (m, r) = v Q m + r • e0 Q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
r : R
⊢ (ι (Q' Q)) (m, r) = (v Q) m + r • e0 Q

Tactic:
rw [e0, v, LinearMap.comp_apply, LinearMap.inl_apply, ← LinearMap.map_smul, Prod.smul_mk,
  smul_zero, smul_eq_mul, mul_one, ← LinearMap.map_add, Prod.mk_add_mk, zero_add, add_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Cones.lean
theorem Cone.w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') :
    c.π.app j ≫ F.map f = c.π.app j'

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ ((const J).obj c.pt).map f ≫ c.π.app j' = c.π.app j'

Tactic:
apply id_comp

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ c.π.app j ≫ F.map f = c.π.app j'

Tactic:
rw [← c.π.naturality f]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ ((const J).obj c.pt).map f ≫ c.π.app j' = c.π.app j'
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem J_det_mul_J_det : det (J l R) * det (J l R) = 1

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (J l R).det * (J l R).det = 1

Tactic:
rw [← det_mul, J_squared, ← one_smul R (-1 : Matrix _ _ R), smul_neg, ← neg_smul, det_smul,
  Fintype.card_sum, det_one, mul_one]

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-1) ^ (Fintype.card l + Fintype.card l) = 1

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-1) ^ (Fintype.card l + Fintype.card l) = 1

Tactic:
apply Even.neg_one_pow

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)

Tactic:
exact Even.add_self _

Result:
no goals
-- Mathlib/Algebra/Homology/HasNoLoop.lean
lemma exists_distinct_next_or :
    (∃ (i : ι), c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬ c.Rel i j

Proof state:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ¬∃ i, c.Rel i j
⊢ ∀ (i : ι), ¬c.Rel i j

Tactic:
simpa using h

Result:
no goals

Proof state:
case pos.intro
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j i : ι
hi : c.Rel i j
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Tactic:
exact Or.inl ⟨i, hi, fun hij ↦ c.not_rel_of_eq hij hi⟩

Result:
no goals

Proof state:
case pos
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ∃ i, c.Rel i j
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Tactic:
obtain ⟨i, hi⟩ := h

Result:
case pos.intro
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j i : ι
hi : c.Rel i j
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Proof state:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Tactic:
by_cases h : ∃ (i : ι), c.Rel i j

Result:
case pos
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ∃ i, c.Rel i j
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

case neg
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ¬∃ i, c.Rel i j
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Proof state:
case neg
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ¬∃ i, c.Rel i j
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Tactic:
exact Or.inr (by simpa using h)

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem IsHilbertSum.mkInternal [∀ i, CompleteSpace <| F i]
    (hFortho : OrthogonalFamily 𝕜 (fun i => F i) fun i => (F i).subtypeₗᵢ)
    (hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure) :
    IsHilbertSum 𝕜 (fun i => F i) fun i => (F i).subtypeₗᵢ :=
  IsHilbertSum.mk hFortho (by simpa [subtypeₗᵢ_toLinearMap, range_subtype] using hFtotal)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(F i)
hFortho : OrthogonalFamily 𝕜 (fun i => ↥(F i)) fun i => (F i).subtypeₗᵢ
hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure
⊢ ⊤ ≤ (⨆ i, LinearMap.range (F i).subtypeₗᵢ.toLinearMap).topologicalClosure

Tactic:
simpa [subtypeₗᵢ_toLinearMap, range_subtype] using hFtotal

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableWithinAt_iff :
    MDifferentiableWithinAt I I' f s x ↔
      ContinuousWithinAt f s x ∧
        DifferentiableWithinAt 𝕜 (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm)
          ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
⊢ MDifferentiableWithinAt I I' f s x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
simp_rw [MDifferentiableWithinAt, ChartedSpace.liftPropWithinAt_iff']

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.uniform_geometric_approx {r' : ℝ≥0}
    (hf : HasFPowerSeriesOnBall f p x r) (h : (r' : ℝ≥0∞) < r) :
    ∃ a ∈ Ioo (0 : ℝ) 1,
      ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
      ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Tactic:
simpa using hf.uniform_geometric_approx h

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem latticeBasis_apply [NumberField K] (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
    latticeBasis K i = (canonicalEmbedding K) (integralBasis K i)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K) i = (canonicalEmbedding K) ((integralBasis K) i)

Tactic:
simp only [latticeBasis, integralBasis_apply, coe_basisOfLinearIndependentOfCardEqFinrank,
  Function.comp_apply, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
    xs.findIdx? p = none ↔ ∀ x, x ∈ xs → p x = false

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } = none ↔ ∀ (x : α), x ∈ { toList := xs } → p x = false

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } = none ↔ ∀ (x : α), x ∈ { toList := xs } → p x = false
-- Mathlib/Topology/Constructions.lean
lemma Pi.induced_restrict_sUnion (𝔖 : Set (Set ι)) :
    induced (⋃₀ 𝔖).restrict (Pi.topologicalSpace (Y := fun i : (⋃₀ 𝔖) ↦ π i)) =
    ⨅ S ∈ 𝔖, induced S.restrict Pi.topologicalSpace

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
𝔖 : Set (Set ι)
⊢ induced (⋃₀ 𝔖).restrict topologicalSpace = ⨅ S ∈ 𝔖, induced S.restrict topologicalSpace

Tactic:
simp_rw [Pi.induced_restrict, iInf_sUnion]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem size_expandIfNecessary [BEq α] [Hashable α] {m : Raw₀ α β} :
    (expandIfNecessary m).val.size = m.val.size

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
⊢ m.expandIfNecessary.val.size = m.val.size

Tactic:
rw [expandIfNecessary]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
⊢ (if Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size then
          ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩
        else
          match expand ⟨m.1.buckets, ⋯⟩ with
          | ⟨buckets', h'⟩ => ⟨{ size := m.1.size, buckets := buckets' }, h'⟩).val.size =
    m.val.size

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
⊢ (if Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size then
          ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩
        else
          match expand ⟨m.1.buckets, ⋯⟩ with
          | ⟨buckets', h'⟩ => ⟨{ size := m.1.size, buckets := buckets' }, h'⟩).val.size =
    m.val.size

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/ModelTheory/LanguageMap.lean
theorem comp_id (F : L →ᴸ L') : F ∘ᴸ LHom.id L = F

Proof state:
case mk
L : Language
L' : Language
onFunction✝ : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation✝ : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ { onFunction := onFunction✝, onRelation := onRelation✝ } ∘ᴸ LHom.id L =
    { onFunction := onFunction✝, onRelation := onRelation✝ }

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
L' : Language
F : L →ᴸ L'
⊢ F ∘ᴸ LHom.id L = F

Tactic:
cases F

Result:
case mk
L : Language
L' : Language
onFunction✝ : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation✝ : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ { onFunction := onFunction✝, onRelation := onRelation✝ } ∘ᴸ LHom.id L =
    { onFunction := onFunction✝, onRelation := onRelation✝ }
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
theorem whiskerLeft_naturality_naturality (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) :
    f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ θ.naturality h =
      f ◁ θ.naturality g ≫ f ◁ θ.app a ◁ H.map₂ β

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : OplaxFunctor B C
θ : OplaxNatTrans G H
a b : B
a' : C
f : a' ⟶ G.obj a
g h : a ⟶ b
β : g ⟶ h
⊢ f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ θ.naturality h = f ◁ θ.naturality g ≫ f ◁ θ.app a ◁ H.map₂ β

Tactic:
simp_rw [← Bicategory.whiskerLeft_comp, naturality_naturality]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Basic.lean
/-- Even though the roots may not span, coroots are distinguished by their pairing with the
roots. The proof depends crucially on the fact that there are finitely-many roots.

Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI. -/
lemma injOn_dualMap_subtype_span_root_coroot [NoZeroSMulDivisors ℤ M] :
    InjOn ((span R (range P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (range P.coroot)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ M
this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.toLin.flip ∘ ⇑P.coroot))
⊢ InjOn (⇑((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (range ⇑P.coroot)

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩ hij

Result:
case intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ M
this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.toLin.flip ∘ ⇑P.coroot))
i j : ι
hij :
  ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (P.coroot i) =
    ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (P.coroot j)
⊢ P.coroot i = P.coroot j

Proof state:
case intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ M
this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.toLin.flip ∘ ⇑P.coroot))
i j : ι
hij :
  ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (P.coroot i) =
    ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (P.coroot j)
⊢ P.coroot i = P.coroot j

Tactic:
exact P.bijectiveRight.injective <| this (mem_range_self i) (mem_range_self j) hij

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ M
⊢ InjOn (⇑((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (range ⇑P.coroot)

Tactic:
have := injOn_dualMap_subtype_span_range_range (finite_range P.root)
  (c := P.toLin.flip ∘ P.coroot) P.root_coroot_two P.mapsTo_reflection_root

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ M
this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.toLin.flip ∘ ⇑P.coroot))
⊢ InjOn (⇑((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (range ⇑P.coroot)
-- Mathlib/Data/Ordering/Lemmas.lean
theorem ite_eq_eq_distrib (c : Prop) [Decidable c] (a b : Ordering) :
    ((if c then a else b) = Ordering.eq) = if c then a = Ordering.eq else b = Ordering.eq

Proof state:
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
by_cases c <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem setRed_toList {t : RBNode α} : t.setRed.toList = t.toList

Proof state:
α : Type u_1
t : RBNode α
⊢ t.setRed.toList = t.toList

Tactic:
cases t <;> simp [setRed]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem id_traverse {α} (xs : List α) : List.traverse (pure : α → Id α) xs = xs

Proof state:
α : Type u_1
xs : List α
⊢ List.traverse pure xs = xs

Tactic:
induction xs <;> simp! [*, List.traverse, functor_norm]

Result:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ cons head✝ <*> tail✝ = head✝ :: tail✝

Proof state:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ cons head✝ <*> tail✝ = head✝ :: tail✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem eventually_prod_nhds_iff {f : Filter ι} {x₀ : α} {p : ι × α → Prop} :
    (∀ᶠ x in f ×ˢ 𝓝 x₀, p x) ↔ ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧
      ∃ ε > 0, ∀ ⦃i⦄, pa i → ∀ ⦃x⦄, dist x x₀ < ε → p (i, x)

Proof state:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]

Result:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Proof state:
case mpr
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)) →
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap

Tactic:
rintro ⟨a1, a2, a3, a4, a5⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ι → Prop
a2 : ∀ᶠ (i : ι) in f, a1 i
a3 : ℝ
a4 : a3 > 0
a5 : ∀ ⦃i : ι⦄, a1 i → ∀ ⦃x : α⦄, dist x x₀ < a3 → p (i, x)
⊢ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap

Proof state:
case mpr.intro.intro.intro.intro
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ι → Prop
a2 : ∀ᶠ (i : ι) in f, a1 i
a3 : ℝ
a4 : a3 > 0
a5 : ∀ ⦃i : ι⦄, a1 i → ∀ ⦃x : α⦄, dist x x₀ < a3 → p (i, x)
⊢ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap

Tactic:
exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_eq_compl_iInter_compl (s : ι → Set β) : ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ

Proof state:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ

Tactic:
simp only [compl_iInter, compl_compl]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem exp_antiperiodic : Function.Antiperiodic exp (π * I)

Proof state:
⊢ Function.Antiperiodic cexp (↑π * I)

Tactic:
simp [exp_add, exp_mul_I]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem true_eq_false : (true = false) = False

Proof state:
⊢ (true = false) = False

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
/--
A monoid is *graphic* if, for all `x` and `y`, the *graphic identity*
`(x * y) * x = x * y` holds.  For a unital shelf, this graphic
identity holds.
-/
lemma act_act_self_eq (x y : S) : (x ◃ y) ◃ x = x ◃ y

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
⊢ (x ◃ y) ◃ x = x ◃ y

Tactic:
rw [h, ← Shelf.self_distrib, act_one]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1

Tactic:
rw [act_one]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = x ◃ y

Tactic:
have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw [act_one]

Result:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
⊢ (x ◃ y) ◃ x = x ◃ y
-- Mathlib/Logic/Equiv/Fin.lean
theorem Fin.preimage_apply_01_prod {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)) :
    (fun f : ∀ i, α i => (f 0, f 1)) ⁻¹' s ×ˢ t =
      Set.pi Set.univ (Fin.cons s <| Fin.cons t finZeroElim)

Proof state:
case h
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
f : (i : Fin 2) → α i
⊢ f ∈ (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t ↔ f ∈ Set.univ.pi (cons s (cons t finZeroElim))

Tactic:
simp [Fin.forall_fin_two]

Result:
no goals

Proof state:
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
⊢ (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi (cons s (cons t finZeroElim))

Tactic:
ext f

Result:
case h
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
f : (i : Fin 2) → α i
⊢ f ∈ (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t ↔ f ∈ Set.univ.pi (cons s (cons t finZeroElim))
-- Mathlib/Algebra/Group/EvenFunction.lean
/-- If `f` is even and `g` is odd, then `f ∘ g` is even. -/
lemma Even.comp_odd [Neg β] {f : β → γ} (hf : f.Even) {g : α → β} (hg : g.Odd) :
    (f ∘ g).Even

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
inst✝ : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = (f ∘ g) a

Tactic:
simp only [comp_apply, hg a, hf _]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
inst✝ : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
⊢ Function.Even (f ∘ g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
inst✝ : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = (f ∘ g) a
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.bind {β γ} {f : α → Part β} {g : α → β → Part γ} (hf : ωScottContinuous f)
    (hg : ωScottContinuous g) : ωScottContinuous fun x ↦ f x >>= g x :=
  ωScottContinuous.of_monotone_map_ωSup
    ⟨hf.monotone.partBind hg.monotone, fun c ↦ by rw [hf.map_ωSup, hg.map_ωSup, ← ωSup_bind]; rfl⟩

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map ({ toFun := f, monotone' := ⋯ }.partBind { toFun := g, monotone' := ⋯ })) =
    ωSup (c.map { toFun := fun x => f x >>= g x, monotone' := ⋯ })

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ f (ωSup c) >>= g (ωSup c) = ωSup (c.map { toFun := fun x => f x >>= g x, monotone' := ⋯ })

Tactic:
rw [hf.map_ωSup, hg.map_ωSup, ← ωSup_bind]

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map ({ toFun := f, monotone' := ⋯ }.partBind { toFun := g, monotone' := ⋯ })) =
    ωSup (c.map { toFun := fun x => f x >>= g x, monotone' := ⋯ })