harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/ConditionalProbability.lean
theorem inter_pos_of_cond_ne_zero (hms : MeasurableSet s) (hcst : μ[t|s] ≠ 0) : 0 < μ (s ∩ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : μ[t | s] ≠ 0
⊢ 0 < μ (s ∩ t)

Tactic:
refine pos_iff_ne_zero.mpr (right_ne_zero_of_mul (a := (μ s)⁻¹) ?_)

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : μ[t | s] ≠ 0
⊢ (μ s)⁻¹ * μ (s ∩ t) ≠ 0

Proof state:
case h.e'_2
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : μ[t | s] ≠ 0
⊢ (μ s)⁻¹ * μ (s ∩ t) = μ[t | s]

Tactic:
simp [hms, Set.inter_comm, cond]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : μ[t | s] ≠ 0
⊢ (μ s)⁻¹ * μ (s ∩ t) ≠ 0

Tactic:
convert hcst

Result:
case h.e'_2
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : μ[t | s] ≠ 0
⊢ (μ s)⁻¹ * μ (s ∩ t) = μ[t | s]
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
/-- The values of an additive character on a ring of positive characteristic are roots of unity. -/
lemma val_mem_rootsOfUnity (φ : AddChar R R') (a : R) (h : 0 < ringChar R) :
    (φ.val_isUnit a).unit ∈ rootsOfUnity (ringChar R).toPNat' R'

Proof state:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
φ : AddChar R R'
a : R
h : 0 < ringChar R
⊢ ⋯.unit ∈ rootsOfUnity (↑(ringChar R).toPNat') R'

Tactic:
simp only [mem_rootsOfUnity', IsUnit.unit_spec, Nat.toPNat'_coe, h, ↓reduceIte,
  ← map_nsmul_eq_pow, nsmul_eq_mul, CharP.cast_eq_zero, zero_mul, map_zero_eq_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem linearCombination_repr : Finsupp.linearCombination _ b (b.repr x) = x

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ ↑b.repr.symm (b.repr x) = x

Tactic:
exact b.repr.symm_apply_apply x

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ (linearCombination R ⇑b) (b.repr x) = x

Tactic:
rw [← b.coe_repr_symm]

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ ↑b.repr.symm (b.repr x) = x
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem newton_seq_succ_dist (n : ℕ) :
    ‖newton_seq (n + 1) - newton_seq n‖ ≤ ‖F.derivative.eval a‖ * T ^ 2 ^ n :=
  calc
    ‖newton_seq (n + 1) - newton_seq n‖ =
        ‖F.eval (newton_seq n)‖ / ‖F.derivative.eval (newton_seq n)‖ :=
      newton_seq_norm_eq hnorm _
    _ = ‖F.eval (newton_seq n)‖ / ‖F.derivative.eval a‖

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval (newton_seq n) (Polynomial.derivative F)‖ =
    ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
rw [newton_seq_deriv_norm]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux2_append (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) :
    (permutationsAux2 t ts nil ys f).2 ++ r = (permutationsAux2 t ts r ys f).2

Proof state:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).2 ++ r = (permutationsAux2 t ts r ys f).2

Tactic:
induction ys generalizing f <;> simp [*]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem get_eq_iff_eq_some {a : Part α} {ha : a.Dom} {b : α} : a.get ha = b ↔ a = some b :=
  ⟨fun h => by simp [h.symm], fun h => by simp [h]⟩

Proof state:
α : Type u_1
a : Part α
ha : a.Dom
b : α
h : a.get ha = b
⊢ a = some b

Tactic:
simp [h.symm]

Result:
no goals

Proof state:
α : Type u_1
a : Part α
ha : a.Dom
b : α
h : a = some b
⊢ a.get ha = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
/-- `Finsupp.mapRange` of a injective function is injective. -/
lemma mapRange_injective (e : M → N) (he₀ : e 0 = 0) (he : Injective e) :
    Injective (Finsupp.mapRange (α := α) e he₀)

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : ∀ (a_1 : α), (mapRange e he₀ a) a_1 = (mapRange e he₀ b) a_1
⊢ ∀ (a_1 : α), a a_1 = b a_1

Tactic:
simpa only [mapRange_apply, he.eq_iff] using h

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : mapRange e he₀ a = mapRange e he₀ b
⊢ a = b

Tactic:
rw [Finsupp.ext_iff] at h ⊢

Result:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : ∀ (a_1 : α), (mapRange e he₀ a) a_1 = (mapRange e he₀ b) a_1
⊢ ∀ (a_1 : α), a a_1 = b a_1

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
⊢ Injective (mapRange e he₀)

Tactic:
intro a b h

Result:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : mapRange e he₀ a = mapRange e he₀ b
⊢ a = b
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuous_iff_le_liminf {f : α → γ} :
    LowerSemicontinuous f ↔ ∀ x, f x ≤ liminf f (𝓝 x)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ liminf f (𝓝 x)

Tactic:
simp only [← lowerSemicontinuousAt_iff_le_liminf, LowerSemicontinuous]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_hom_hom_inv_hom_hom :
    (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv =
      (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv) =
    inv ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Extr.lean
theorem IsMinOn.sub (hf : IsMinOn f s a) (hg : IsMaxOn g s a) :
    IsMinOn (fun x => f x - g x) s a

Proof state:
α : Type u
β : Type v
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMaxOn g s a
⊢ IsMinOn (fun x => f x - g x) s a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem parts_nonempty_iff : P.parts.Nonempty ↔ a ≠ ⊥

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts.Nonempty ↔ a ≠ ⊥

Tactic:
rw [nonempty_iff_ne_empty, not_iff_not, parts_eq_empty_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem bot_eq_top_iff_finrank_eq_one [Nontrivial E] [Module.Free F E] :
    (⊥ : Subalgebra F E) = ⊤ ↔ finrank F E = 1

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F E
⊢ ⊥ = ⊤ ↔ finrank F E = 1

Tactic:
haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F E
this : Free F ↥⊤
⊢ ⊥ = ⊤ ↔ finrank F E = 1

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F E
this : Free F ↥⊤
⊢ ⊥ = ⊤ ↔ finrank F E = 1

Tactic:
rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
  Subalgebra.finrank_eq_one_iff, eq_comm]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
@[symm]
protected lemma symm : q.IsConjExponent p where
  inv_add_inv_conj

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ q⁻¹ + p⁻¹ = 1

Tactic:
simpa [add_comm] using h.inv_add_inv_conj

Result:
no goals
-- Mathlib/CategoryTheory/Action/Basic.lean
theorem Iso.conj_ρ {M N : Action V G} (f : M ≅ N) (g : G) :
    N.ρ g = ((forget V G).mapIso f).conj (M.ρ g)

Proof state:
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : Type u
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
g : G
⊢ ((forget V G).mapIso f).hom ≫ N.ρ g = M.ρ g ≫ ((forget V G).mapIso f).hom

Tactic:
simp [f.hom.comm]

Result:
no goals

Proof state:
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : Type u
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
g : G
⊢ N.ρ g = ((forget V G).mapIso f).conj (M.ρ g)

Tactic:
rw [Iso.conj_apply, Iso.eq_inv_comp]

Result:
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : Type u
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
g : G
⊢ ((forget V G).mapIso f).hom ≫ N.ρ g = M.ρ g ≫ ((forget V G).mapIso f).hom
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem smul_cancel {r : X} {s t : S} : ((s : R) /ₒ t) • (r /ₒ s) = r /ₒ t

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ (↑s /ₒ t) • (r /ₒ s) = r /ₒ t

Tactic:
simp [oreDiv_smul_char s.1 r t s 1 1 (by simp)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem diagonalObjPullbackFstIso_inv_snd_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (diagonalObjPullbackFstIso f g).inv ≫ pullback.snd _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      snd (fst f g) (fst f g) ≫ snd f g =
    fst (snd g g ≫ g) f ≫ snd g g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ snd (fst f g) (fst f g) ≫ snd f g = fst (snd g g ≫ g) f ≫ snd g g

Tactic:
delta diagonalObjPullbackFstIso

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      snd (fst f g) (fst f g) ≫ snd f g =
    fst (snd g g ≫ g) f ≫ snd g g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b

Proof state:
α : Type u_1
a b : α
inst✝ : BEq α
lt : α → α → Bool
⊢ (do
        let r ←
          forIn' { start := 0, stop := 1, step := 1, step_pos := Nat.zero_lt_one } ⟨none, PUnit.unit⟩ fun i h r =>
              if lt a b = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (a != b) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure false
          | some a => pure a).run =
    lt a b

Tactic:
cases lt a b <;> cases a != b <;> simp [Id.run]

Result:
no goals

Proof state:
α : Type u_1
a b : α
inst✝ : BEq α
lt : α → α → Bool
⊢ { toArray := #[a], size_toArray := ⋯ }.lex { toArray := #[b], size_toArray := ⋯ } lt = lt a b

Tactic:
simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton]

Result:
α : Type u_1
a b : α
inst✝ : BEq α
lt : α → α → Bool
⊢ (do
        let r ←
          forIn' { start := 0, stop := 1, step := 1, step_pos := Nat.zero_lt_one } ⟨none, PUnit.unit⟩ fun i h r =>
              if lt a b = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (a != b) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure false
          | some a => pure a).run =
    lt a b
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem inv_subset_closure (S : Set G) : S⁻¹ ⊆ closure S := fun s hs => by
  rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
  exact subset_closure (mem_inv.mp hs)

Proof state:
G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s⁻¹ ∈ closure S

Tactic:
exact subset_closure (mem_inv.mp hs)

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)

Tactic:
rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]

Result:
G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s⁻¹ ∈ closure S
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_insert_insert_insert_of_mem_affineSpan_pair {p₁ p₂ p₃ p₄ p₅ : P}
    (h₁ : p₁ ∈ line[k, p₄, p₅]) (h₂ : p₂ ∈ line[k, p₄, p₅]) (h₃ : p₃ ∈ line[k, p₄, p₅]) :
    Collinear k ({p₁, p₂, p₃, p₄, p₅} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₁, p₂, p₃, p₄, p₅}

Tactic:
rw [collinear_insert_iff_of_mem_affineSpan
    ((AffineSubspace.le_def' _ _).1
      (affineSpan_mono k ((Set.subset_insert _ _).trans (Set.subset_insert _ _))) _ h₁),
  collinear_insert_iff_of_mem_affineSpan
    ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k (Set.subset_insert _ _)) _ h₂),
  collinear_insert_iff_of_mem_affineSpan h₃]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₄, p₅}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₄, p₅}

Tactic:
exact collinear_pair _ _ _

Result:
no goals
-- Mathlib/Order/Cover.lean
lemma covBy_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t :=
  ⟨CovBy.exists_set_insert, by rintro ⟨a, ha, rfl⟩; exact covBy_insert ha⟩

Proof state:
case intro.intro
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s

Tactic:
exact covBy_insert ha

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
⊢ (∃ a ∉ s, insert a s = t) → s ⋖ t

Tactic:
rintro ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
@[simp] lemma toNNRealLinear_inj (Λ₁ Λ₂ : C_c(α, ℝ) →ₗ[ℝ] ℝ) (hΛ₁ hΛ₂) :
    toNNRealLinear Λ₁ hΛ₁ = toNNRealLinear Λ₂ hΛ₂ ↔ Λ₁ = Λ₂

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
h : ∀ (x : α →C_c ℝ), Λ₁ x = Λ₂ x
f : α →C_c ℝ≥0
⊢ Λ₁ f.toReal = Λ₂ f.toReal

Tactic:
rw [LinearMap.ext h]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
⊢ toNNRealLinear Λ₁ hΛ₁ = toNNRealLinear Λ₂ hΛ₂ ↔ Λ₁ = Λ₂

Tactic:
simp only [LinearMap.ext_iff, NNReal.eq_iff, toNNRealLinear_apply]

Result:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
⊢ (∀ (x : α →C_c ℝ≥0), Λ₁ x.toReal = Λ₂ x.toReal) ↔ ∀ (x : α →C_c ℝ), Λ₁ x = Λ₂ x

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
h : ∀ (x : α →C_c ℝ≥0), Λ₁ x.toReal = Λ₂ x.toReal
f : α →C_c ℝ
⊢ Λ₁ f = Λ₂ f

Tactic:
rw [← nnrealPart_sub_nnrealPart_neg f]

Result:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
h : ∀ (x : α →C_c ℝ≥0), Λ₁ x.toReal = Λ₂ x.toReal
f : α →C_c ℝ
⊢ Λ₁ (f.nnrealPart.toReal - (-f).nnrealPart.toReal) = Λ₂ (f.nnrealPart.toReal - (-f).nnrealPart.toReal)

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
⊢ (∀ (x : α →C_c ℝ≥0), Λ₁ x.toReal = Λ₂ x.toReal) ↔ ∀ (x : α →C_c ℝ), Λ₁ x = Λ₂ x

Tactic:
refine ⟨fun h f ↦ ?_, fun h f ↦ by rw [LinearMap.ext h]⟩

Result:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
h : ∀ (x : α →C_c ℝ≥0), Λ₁ x.toReal = Λ₂ x.toReal
f : α →C_c ℝ
⊢ Λ₁ f = Λ₂ f

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₗ[ℝ] ℝ
hΛ₁ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₁ f
hΛ₂ : ∀ (f : α →C_c ℝ), 0 ≤ f → 0 ≤ Λ₂ f
h : ∀ (x : α →C_c ℝ≥0), Λ₁ x.toReal = Λ₂ x.toReal
f : α →C_c ℝ
⊢ Λ₁ (f.nnrealPart.toReal - (-f).nnrealPart.toReal) = Λ₂ (f.nnrealPart.toReal - (-f).nnrealPart.toReal)

Tactic:
simp_rw [map_sub, h]

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem invertible_unique {α : Type u} [Monoid α] (a b : α) [Invertible a] [Invertible b]
    (h : a = b) : ⅟ a = ⅟ b

Proof state:
case hac
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ a * ⅟b = 1

Tactic:
rw [h, mul_invOf_self]

Result:
no goals

Proof state:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b

Tactic:
apply invOf_eq_right_inv

Result:
case hac
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ a * ⅟b = 1
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
lemma comp_apply {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) (r : M) :
    (f ≫ g) r = g (f r)

Proof state:
M N O : SemiNormedGrp
f : M ⟶ N
g : N ⟶ O
r : M.carrier
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem eq_zero_of_forall_not_mem {s : Multiset α} : (∀ x, x ∉ s) → s = 0 :=
  Quot.inductionOn s fun l H => by rw [eq_nil_iff_forall_not_mem.mpr H]; rfl

Proof state:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk (⇑(isSetoid α)) l = 0

Tactic:
rw [eq_nil_iff_forall_not_mem.mpr H]

Result:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0

Proof state:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
@[continuity, fun_prop]
lemma continuous_sumAssoc_symm : Continuous (Equiv.sumAssoc X Y Z).symm :=
  Continuous.sumElim (by fun_prop) (by fun_prop)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)

Tactic:
fun_prop

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous (Sum.inl ∘ Sum.inl)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropOn_of_mem_maximalAtlas [HasGroupoid M G] (hG : G.LocalInvariantProp G Q)
    (hQ : ∀ y, Q id univ y) (he : e ∈ maximalAtlas M G) : LiftPropOn Q e e.source

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : M
hx : x ∈ e.source
⊢ LiftPropWithinAt Q (↑e) e.source x

Tactic:
apply hG.liftPropWithinAt_of_liftPropAt_of_mem_nhds (hG.liftPropAt_of_mem_maximalAtlas hQ he hx)

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : M
hx : x ∈ e.source
⊢ e.source ∈ 𝓝 x

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
⊢ LiftPropOn Q (↑e) e.source

Tactic:
intro x hx

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : M
hx : x ∈ e.source
⊢ LiftPropWithinAt Q (↑e) e.source x

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : M
hx : x ∈ e.source
⊢ e.source ∈ 𝓝 x

Tactic:
exact e.open_source.mem_nhds hx

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
lemma hasTensor_of_iso {X₁ X₂ Y₁ Y₂ : GradedObject I C}
    (e₁ : X₁ ≅ Y₁) (e₂ : X₂ ≅ Y₂) [HasTensor X₁ X₂] :
    HasTensor Y₁ Y₂

Proof state:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
e₁ : X₁ ≅ Y₁
e₂ : X₂ ≅ Y₂
inst✝ : X₁.HasTensor X₂
e : ((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂ ≅ ((mapBifunctor (curriedTensor C) I I).obj Y₁).obj Y₂ :=
  (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).isoMk (((mapBifunctor (curriedTensor C) I I).obj Y₁).obj Y₂)
    fun x =>
    match x with
    | (i, j) => (eval i).mapIso e₁ ⊗ (eval j).mapIso e₂
⊢ Y₁.HasTensor Y₂

Tactic:
exact hasMap_of_iso e _

Result:
no goals

Proof state:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
e₁ : X₁ ≅ Y₁
e₂ : X₂ ≅ Y₂
inst✝ : X₁.HasTensor X₂
⊢ Y₁.HasTensor Y₂

Tactic:
let e : ((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂ ≅
  ((mapBifunctor (curriedTensor C) I I).obj Y₁).obj Y₂ := isoMk _ _
    (fun ⟨i, j⟩ ↦ (eval i).mapIso e₁ ⊗ (eval j).mapIso e₂)

Result:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
e₁ : X₁ ≅ Y₁
e₂ : X₂ ≅ Y₂
inst✝ : X₁.HasTensor X₂
e : ((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂ ≅ ((mapBifunctor (curriedTensor C) I I).obj Y₁).obj Y₂ :=
  (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).isoMk (((mapBifunctor (curriedTensor C) I I).obj Y₁).obj Y₂)
    fun x =>
    match x with
    | (i, j) => (eval i).mapIso e₁ ⊗ (eval j).mapIso e₂
⊢ Y₁.HasTensor Y₂
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_le_one' (h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 :=
  (prod_le_prod' h).trans_eq (by rw [prod_const_one])

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
h : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, 1 = 1

Tactic:
rw [prod_const_one]

Result:
no goals