harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma prod_apply (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
    (a : α) :
    (κ ×ₖ η) a = (κ a).prod (η a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
⊢ (κ ×ₖ η) a = (κ a).prod (η a)

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ×ₖ η) a) s = ((κ a).prod (η a)) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η a) {c | (b, c) ∈ s} ∂κ a = ∫⁻ (x : β), (η a) (Prod.mk x ⁻¹' s) ∂κ a

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ×ₖ η) a) s = ((κ a).prod (η a)) s

Tactic:
rw [prod_apply' _ _ _ hs, Measure.prod_apply hs]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η a) {c | (b, c) ∈ s} ∂κ a = ∫⁻ (x : β), (η a) (Prod.mk x ⁻¹' s) ∂κ a
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_one_left (n : ℕ) : uniformBell 1 n = 1

Proof state:
n : ℕ
⊢ uniformBell 1 n = 1

Tactic:
simp only [uniformBell_eq, Finset.range_one, Finset.prod_singleton, zero_mul,
  zero_add, choose_self]

Result:
no goals
-- Mathlib/Algebra/Module/SpanRank.lean
lemma spanFinrank_eq_iInf (p : Submodule R M) :
    p.spanFinrank = ⨅ (s : {s : Set M // s.Finite ∧ span R s = p}), s.2.1.toFinset.card

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.spanFinrank = ⨅ s, ⋯.toFinset.card

Tactic:
simp [spanFinrank, Cardinal.toNat, spanRank_toENat_eq_iInf_finset_card, ENat.iInf_toNat]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem algebraMap_injective : Function.Injective (algebraMap K[X] (RatFunc K))

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (ofFractionRing ∘ ⇑(algebraMap K[X] (FractionRing K[X])))

Tactic:
exact ofFractionRing_injective.comp (IsFractionRing.injective _ _)

Result:
no goals

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective ⇑(algebraMap K[X] (RatFunc K))

Tactic:
rw [← ofFractionRing_comp_algebraMap]

Result:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (ofFractionRing ∘ ⇑(algebraMap K[X] (FractionRing K[X])))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_eq_true_of_lo (u v k : Nat) : u + k ≤ v → (u ≤ v) = True :=
  by simp; omega

Proof state:
u v k : Nat
⊢ u + k ≤ v → u ≤ v

Tactic:
omega

Result:
no goals

Proof state:
u v k : Nat
⊢ u + k ≤ v → (u ≤ v) = True

Tactic:
simp

Result:
u v k : Nat
⊢ u + k ≤ v → u ≤ v
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
/-- If `F` has odd characteristic, then `quadraticChar F` takes the value `-1` on some unit. -/
lemma quadraticChar_exists_neg_one' (hF : ringChar F ≠ 2) : ∃ a : Fˣ, quadraticChar F a = -1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
x✝ : ∃ a, (quadraticChar F) a = -1
a : F
ha : (quadraticChar F) a = -1
⊢ IsUnit a

Tactic:
contrapose ha

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
x✝ : ∃ a, (quadraticChar F) a = -1
a : F
ha : ¬IsUnit a
⊢ ¬(quadraticChar F) a = -1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
x✝ : ∃ a, (quadraticChar F) a = -1
a : F
ha : ¬IsUnit a
⊢ ¬(quadraticChar F) a = -1

Tactic:
exact ne_of_eq_of_ne ((quadraticChar F).map_nonunit ha) (mt zero_eq_neg.mp one_ne_zero)

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ ∃ a, (quadraticChar F) ↑a = -1

Tactic:
refine (fun ⟨a, ha⟩ ↦ ⟨IsUnit.unit ?_, ha⟩) (quadraticChar_exists_neg_one hF)

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
x✝ : ∃ a, (quadraticChar F) a = -1
a : F
ha : (quadraticChar F) a = -1
⊢ IsUnit a
-- Mathlib/Order/InitialSeg.lean
theorem toRelEmbedding_injective [IsIrrefl β s] [IsTrichotomous β s] :
    Function.Injective (@toRelEmbedding α β r s)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
⊢ Injective toRelEmbedding

Tactic:
rintro ⟨f, a, hf⟩ ⟨g, b, hg⟩ rfl

Result:
case mk.mk
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
⊢ { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf } =
    { toRelEmbedding := { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding, top := b,
      mem_range_iff_rel' := hg }

Proof state:
case mk.mk.e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
⊢ a = b

Tactic:
refine extensional_of_trichotomous_of_irrefl s fun x ↦ ?_

Result:
case mk.mk.e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ s x a ↔ s x b

Proof state:
case mk.mk.e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ s x a ↔ s x b

Tactic:
rw [← hf, hg]

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
⊢ { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf } =
    { toRelEmbedding := { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding, top := b,
      mem_range_iff_rel' := hg }

Tactic:
congr

Result:
case mk.mk.e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
⊢ a = b
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_smul_real_nonneg (s : SignedMeasure α) (r : ℝ)
    (hr : 0 ≤ r) : (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
lift r to ℝ≥0 using hr

Result:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (↑r • s).toJordanDecomposition = ↑r • s.toJordanDecomposition

Proof state:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (↑r • s).toJordanDecomposition = ↑r • s.toJordanDecomposition

Tactic:
rw [JordanDecomposition.coe_smul, ← toJordanDecomposition_smul]

Result:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (↑r • s).toJordanDecomposition = (r • s).toJordanDecomposition

Proof state:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (↑r • s).toJordanDecomposition = (r • s).toJordanDecomposition

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem rupUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
    (insert f c).rupUnits = f.rupUnits

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).rupUnits = f.rupUnits

Tactic:
simp only [insert]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).rupUnits =
    f.rupUnits

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).rupUnits =
    f.rupUnits

Tactic:
split <;> simp only

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem mk0_inj {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) : Units.mk0 a ha = Units.mk0 b hb ↔ a = b :=
  ⟨fun h => by injection h, fun h => Units.ext h⟩

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
h : mk0 a ha = mk0 b hb
⊢ a = b

Tactic:
injection h

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem continuousWithinAt_dslope_of_ne (h : b ≠ a) :
    ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (dslope f a) s b

Tactic:
simp only [dslope, continuousWithinAt_update_of_ne h]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (slope f a) s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (dslope f a) s b

Tactic:
classical
simp only [dslope, continuousWithinAt_update_of_ne h]
exact ((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul
  (hc.sub continuousWithinAt_const)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b

Tactic:
refine ⟨ContinuousWithinAt.of_dslope, fun hc => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (dslope f a) s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (slope f a) s b

Tactic:
exact ((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul
  (hc.sub continuousWithinAt_const)

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem lift_of (f : ∀ i, G i →* K) (k : H →* K)
    (hf : ∀ i, (f i).comp (φ i) = k)
    {i : ι} (g : G i) : (lift f k hf) (of i g : PushoutI φ) = f i g

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
g : G i
⊢ ((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp (inl.comp CoprodI.of)) g) = (f i) g

Tactic:
simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe,
  lift_apply_inl, CoprodI.lift_of]

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
g : G i
⊢ (lift f k hf) ((of i) g) = (f i) g

Tactic:
delta PushoutI lift of

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
g : G i
⊢ ((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp (inl.comp CoprodI.of)) g) = (f i) g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf_cons [BEq α] :
    (x :: xs : List α).idxOf y = bif x == y then 0 else xs.idxOf y + 1

Proof state:
α : Type u_1
x : α
xs : List α
y : α
inst✝ : BEq α
⊢ idxOf y (x :: xs) = bif x == y then 0 else idxOf y xs + 1

Tactic:
dsimp [idxOf]

Result:
α : Type u_1
x : α
xs : List α
y : α
inst✝ : BEq α
⊢ findIdx (fun x => x == y) (x :: xs) = bif x == y then 0 else findIdx (fun x => x == y) xs + 1

Proof state:
α : Type u_1
x : α
xs : List α
y : α
inst✝ : BEq α
⊢ findIdx (fun x => x == y) (x :: xs) = bif x == y then 0 else findIdx (fun x => x == y) xs + 1

Tactic:
simp [findIdx_cons]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem boxProd_adj_left {a₁ : α} {b : β} {a₂ : α} :
    (G □ H).Adj (a₁, b) (a₂, b) ↔ G.Adj a₁ a₂

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ : α
b : β
a₂ : α
⊢ (G □ H).Adj (a₁, b) (a₂, b) ↔ G.Adj a₁ a₂

Tactic:
simp only [boxProd_adj, and_true, SimpleGraph.irrefl, false_and, or_false]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
@[simp]
lemma w_obj (F : 𝒳 ⥤ᵇ 𝒴) (a : 𝒳.obj) : 𝒴.p.obj (F.obj a) = 𝒳.p.obj a

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ 𝒴.p.obj (F.obj a) = 𝒳.p.obj a

Tactic:
rw [← Functor.comp_obj, F.w]

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem strictMonoOn_dual_iff :
    StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictMonoOn f s

Tactic:
rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
theorem universally_le (P : MorphismProperty C) : P.universally ≤ P

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
rw [Category.comp_id, Category.id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.universally ≤ P

Tactic:
intro X Y f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ P f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ P f

Tactic:
exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem alternatingProd_cons_cons [DivInvMonoid α] (a b : α) (l : List α) :
    alternatingProd (a :: b :: l) = a / b * alternatingProd l

Proof state:
α : Type u_2
inst✝ : DivInvMonoid α
a b : α
l : List α
⊢ (a :: b :: l).alternatingProd = a / b * l.alternatingProd

Tactic:
rw [div_eq_mul_inv, alternatingProd_cons_cons']

Result:
no goals
-- Mathlib/RingTheory/Norm/Defs.lean
theorem norm_algebraMap {L : Type*} [Ring L] [Algebra K L] (x : K) :
    norm K (algebraMap K L x) = x ^ finrank K L

Proof state:
case pos
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ∃ s, Nonempty (Basis { x // x ∈ s } K L)
⊢ (norm K) ((algebraMap K L) x) = x ^ finrank K L

Tactic:
rw [norm_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]

Result:
no goals

Proof state:
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
⊢ (norm K) ((algebraMap K L) x) = x ^ finrank K L

Tactic:
by_cases H : ∃ s : Finset L, Nonempty (Basis s K L)

Result:
case pos
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ∃ s, Nonempty (Basis { x // x ∈ s } K L)
⊢ (norm K) ((algebraMap K L) x) = x ^ finrank K L

case neg
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } K L)
⊢ (norm K) ((algebraMap K L) x) = x ^ finrank K L

Proof state:
case neg.intro.intro
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } K L)
s : Finset L
b : Basis (↑↑s) K L
⊢ False

Tactic:
exact H ⟨s, ⟨b⟩⟩

Result:
no goals

Proof state:
case neg
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } K L)
⊢ ¬∃ s, Nonempty (Basis (↑↑s) K L)

Tactic:
rintro ⟨s, ⟨b⟩⟩

Result:
case neg.intro.intro
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } K L)
s : Finset L
b : Basis (↑↑s) K L
⊢ False

Proof state:
case neg
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } K L)
⊢ (norm K) ((algebraMap K L) x) = x ^ finrank K L

Tactic:
rw [norm_eq_one_of_not_exists_basis K H, finrank_eq_zero_of_not_exists_basis, pow_zero]

Result:
case neg
K : Type u_3
inst✝² : Field K
L : Type u_4
inst✝¹ : Ring L
inst✝ : Algebra K L
x : K
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } K L)
⊢ ¬∃ s, Nonempty (Basis (↑↑s) K L)
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iUnion_right (s : Set α) (t : ι → Set β) :
    image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i)

Tactic:
simp only [← image_prod, prod_iUnion, image_iUnion]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem map_iInf {ι β} {f : α → β} (hf : Injective f) (m : ι → OuterMeasure α) :
    map f (⨅ i, m i) = restrict (range f) (⨅ i, map f (m i))

Proof state:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ (map f) (⨅ i, m i) = (map f) ((comap f) (⨅ i, (map f) (m i)))

Tactic:
simp only [comap_iInf, comap_map hf]

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ (map f) (⨅ i, m i) = (restrict (range f)) (⨅ i, (map f) (m i))

Tactic:
refine Eq.trans ?_ (map_comap _ _)

Result:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ (map f) (⨅ i, m i) = (map f) ((comap f) (⨅ i, (map f) (m i)))
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem LieGroup.of_le {m n : WithTop ℕ∞} (hmn : m ≤ n)
    [h : LieGroup I n G] : LieGroup I m G

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : Group G
m n : WithTop ℕ∞
hmn : m ≤ n
h : LieGroup I n G
this : ContMDiffMul I m G
⊢ LieGroup I m G

Tactic:
exact ⟨h.contMDiff_inv.of_le hmn⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : Group G
m n : WithTop ℕ∞
hmn : m ≤ n
h : LieGroup I n G
⊢ LieGroup I m G

Tactic:
have : ContMDiffMul I m G := ContMDiffMul.of_le hmn

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : Group G
m n : WithTop ℕ∞
hmn : m ≤ n
h : LieGroup I n G
this : ContMDiffMul I m G
⊢ LieGroup I m G
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_getD_default [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.get! a = m.getD a default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.get! a = m.getD a default

Tactic:
simp_to_raw using Raw₀.get!_eq_getD_default

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem coe_sSup_of_directedOn {S : Set (NonUnitalSubring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem comp_surjective {f : A →+* B} {g : B →+* C} (hf : f.FiniteType) (hg : Surjective g) :
    (g.comp f).FiniteType

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : f.FiniteType
hg : Surjective ⇑g
⊢ (g.comp f).FiniteType

Tactic:
algebraize_only [f, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : f.FiniteType
hg : Surjective ⇑g
algInst✝¹ : Algebra A B := f.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
⊢ (g.comp f).FiniteType

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : f.FiniteType
hg : Surjective ⇑g
algInst✝¹ : Algebra A B := f.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
⊢ (g.comp f).FiniteType

Tactic:
exact Algebra.FiniteType.of_surjective hf
  { g with
    toFun := g
    commutes' := fun a => rfl }
  hg

Result:
no goals