harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
theorem comp_add (f : X ⟶ Y) (g h : Y ⟶ Z) : f ≫ (g + h) = f ≫ g + f ≫ h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ (f ≫ biprod.lift g h) ≫ biprod.desc (𝟙 Z) (𝟙 Z) = biprod.lift (f ≫ g) (f ≫ h) ≫ biprod.desc (𝟙 Z) (𝟙 Z)

Tactic:
congr

Result:
case e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ biprod.lift g h = biprod.lift (f ≫ g) (f ≫ h)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
simp only [add_eq_left_addition, ← Category.assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ (f ≫ biprod.lift g h) ≫ biprod.desc (𝟙 Z) (𝟙 Z) = biprod.lift (f ≫ g) (f ≫ h) ≫ biprod.desc (𝟙 Z) (𝟙 Z)

Proof state:
case e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ biprod.lift g h = biprod.lift (f ≫ g) (f ≫ h)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
lemma finsuppAntidiag_empty (n : μ) :
    finsuppAntidiag (∅ : Finset ι) n = if n = 0 then {0} else ∅

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ ∅.finsuppAntidiag n = if n = 0 then {0} else ∅

Tactic:
split_ifs with hn <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem transcendental_aeval_iff {r : A} {f : K[X]} :
    Transcendental K (Polynomial.aeval r f) ↔ Transcendental K r ∧ Transcendental K f

Proof state:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : IsIntegral K r
⊢ IsIntegral K ((aeval r) f)

Tactic:
exact .of_mem_of_fg _ h.fg_adjoin_singleton _ (aeval_mem_adjoin_singleton _ _)

Result:
no goals

Proof state:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
⊢ Transcendental K ((aeval r) f) ↔ Transcendental K r ∧ Transcendental K f

Tactic:
refine ⟨fun h ↦ ⟨?_, h.of_aeval⟩, fun ⟨h1, h2⟩ ↦ h1.aeval_of_transcendental h2⟩

Result:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : Transcendental K ((aeval r) f)
⊢ Transcendental K r

Proof state:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : Transcendental K ((aeval r) f)
⊢ Transcendental K r

Tactic:
rw [Transcendental] at h ⊢

Result:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : ¬IsAlgebraic K ((aeval r) f)
⊢ ¬IsAlgebraic K r

Proof state:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : ¬IsAlgebraic K ((aeval r) f)
⊢ ¬IsAlgebraic K r

Tactic:
contrapose! h

Result:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : IsAlgebraic K r
⊢ IsAlgebraic K ((aeval r) f)

Proof state:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : IsAlgebraic K r
⊢ IsAlgebraic K ((aeval r) f)

Tactic:
rw [isAlgebraic_iff_isIntegral] at h ⊢

Result:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : IsIntegral K r
⊢ IsIntegral K ((aeval r) f)
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSupIndep_of_dfinsupp_sumAddHom_injective' (p : ι → AddSubgroup N)
    (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
⊢ iSupIndep p

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]

Result:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
⊢ iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
⊢ iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)

Tactic:
exact iSupIndep_of_dfinsupp_lsum_injective _ h

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem minimal_and_iff_right_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) :
    Minimal (fun x ↦ P x ∧ Q x) x ↔ (Minimal P x) ∧ Q x

Proof state:
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x => P x ∧ Q x) x ↔ Minimal P x ∧ Q x

Tactic:
simp_rw [and_iff_left_of_imp (fun x ↦ hPQ x), iff_self_and]

Result:
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x => P x) x → Q x

Proof state:
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x => P x) x → Q x

Tactic:
exact fun h ↦ hPQ h.prop

Result:
no goals
-- Mathlib/Probability/Process/PartitionFiltration.lean
lemma iSup_partitionFiltration (ht : ∀ n, MeasurableSet (t n))
    (ht_range : generateFrom (Set.range t) = m) :
    ⨆ n, partitionFiltration ht n = m

Proof state:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
ht_range : generateFrom (Set.range t) = m
⊢ ⨆ n, ↑(partitionFiltration ht) n = m

Tactic:
rw [iSup_partitionFiltration_eq_generateFrom_range ht, ht_range]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_ceil_right (n : ℤ) :
    Tendsto (fun x => ceil x : α → α) (𝓝[>] n) (𝓝[≥] (n + 1)) :=
  ((tendsto_pure_pure _ _).comp (tendsto_ceil_right_pure_add_one n)).mono_right <| by
    rw [← @cast_one α, ← cast_add]; exact pure_le_nhdsWithin le_rfl

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] (↑n + 1)

Tactic:
rw [← @cast_one α, ← cast_add]

Result:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] ↑(n + 1)

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] ↑(n + 1)

Tactic:
exact pure_le_nhdsWithin le_rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem HasFPowerSeriesAt.eq_formalMultilinearSeries {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E}
    {f : 𝕜 → E} {x : 𝕜} (h₁ : HasFPowerSeriesAt f p₁ x) (h₂ : HasFPowerSeriesAt f p₂ x) : p₁ = p₂ :=
  sub_eq_zero.mp (HasFPowerSeriesAt.eq_zero (x := x) (by simpa only [sub_self] using h₁.sub h₂))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : HasFPowerSeriesAt f p₁ x
h₂ : HasFPowerSeriesAt f p₂ x
⊢ HasFPowerSeriesAt 0 (p₁ - p₂) x

Tactic:
simpa only [sub_self] using h₁.sub h₂

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_le_iff_sq_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2

Proof state:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2

Tactic:
rw [sq, sq]

Result:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Proof state:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
exact natAbs_le_iff_mul_self_le

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem filter_pos_add_filter_neg [AddZeroClass M] (f : α →₀ M) (p : α → Prop) [DecidablePred p] :
    (f.filter p + f.filter fun a => ¬p a) = f :=
  DFunLike.coe_injective <| by
    simp only [coe_add, filter_eq_indicator]
    exact Set.indicator_self_add_compl { x | p x } f

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ (fun f => ⇑f) (filter p f + filter (fun a => ¬p a) f) = (fun f => ⇑f) f

Tactic:
simp only [coe_add, filter_eq_indicator]

Result:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ {x | p x}.indicator ⇑f + {a | ¬p a}.indicator ⇑f = ⇑f

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ {x | p x}.indicator ⇑f + {a | ¬p a}.indicator ⇑f = ⇑f

Tactic:
exact Set.indicator_self_add_compl { x | p x } f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem foldr_pmap (l : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x

Proof state:
α : Type u_1
n : Nat
β : Type u_2
γ : Type u_3
l : Vector α n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
g : β → γ → γ
x : γ
⊢ foldr g x (pmap f l H) = foldr (fun a acc => g (f a.val ⋯) acc) x l.attach

Tactic:
rw [pmap_eq_map_attach, foldr_map]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive (attr := simp)]
lemma inv_op_smul_set_distrib (a : α) (s : Set α) : (op a • s)⁻¹ = a⁻¹ • s⁻¹

Proof state:
case h
α : Type u_2
inst✝ : Group α
a : α
s : Set α
x✝ : α
⊢ x✝ ∈ (op a • s)⁻¹ ↔ x✝ ∈ a⁻¹ • s⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
a : α
s : Set α
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : Group α
a : α
s : Set α
x✝ : α
⊢ x✝ ∈ (op a • s)⁻¹ ↔ x✝ ∈ a⁻¹ • s⁻¹
-- Mathlib/NumberTheory/NumberField/EquivReindex.lean
theorem canonicalEmbedding_eq_basisMatrix_mulVec (α : K) :
    canonicalEmbedding K α = (basisMatrix K).transpose.mulVec
      (fun i ↦ (((integralBasis K).reindex (equivReindex K).symm).repr α i : ℂ))

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
i : K →+* ℂ
⊢ (canonicalEmbedding K) α i =
    ((basisMatrix K)ᵀ *ᵥ fun i => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)) i

Tactic:
rw [← (latticeBasis K).sum_repr (canonicalEmbedding K α), ← Equiv.sum_comp (equivReindex K)]

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
i : K →+* ℂ
⊢ (∑ i : K →+* ℂ,
        ((latticeBasis K).repr ((canonicalEmbedding K) α)) ((equivReindex K) i) • (latticeBasis K) ((equivReindex K) i))
      i =
    ((basisMatrix K)ᵀ *ᵥ fun i => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)) i

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
⊢ (canonicalEmbedding K) α =
    (basisMatrix K)ᵀ *ᵥ fun i => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)

Tactic:
ext i

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
i : K →+* ℂ
⊢ (canonicalEmbedding K) α i =
    ((basisMatrix K)ᵀ *ᵥ fun i => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)) i

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
i : K →+* ℂ
⊢ (∑ i : K →+* ℂ,
        ((latticeBasis K).repr ((canonicalEmbedding K) α)) ((equivReindex K) i) • (latticeBasis K) ((equivReindex K) i))
      i =
    ((basisMatrix K)ᵀ *ᵥ fun i => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)) i

Tactic:
simp only [canonicalEmbedding.integralBasis_repr_apply, mulVec, dotProduct,
  transpose_apply, of_apply, Fintype.sum_apply, mul_comm, Basis.repr_reindex,
  Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Pi.smul_apply, smul_eq_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.not_adj_left_of_ne {M : Subgraph G} {u v w : V} (hM : M.IsMatching) (huv : v ≠ w)
    (hadj : M.Adj u v) : ¬M.Adj u w

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huv : v ≠ w
hadj : M.Adj u v
⊢ ¬M.Adj u w

Tactic:
intro hadj'

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huv : v ≠ w
hadj : M.Adj u v
hadj' : M.Adj u w
⊢ False

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huv : v ≠ w
hadj : M.Adj u v
hadj' : M.Adj u w
x : V
hx : (fun w => M.Adj u w) x ∧ ∀ (y : V), (fun w => M.Adj u w) y → y = x
⊢ False

Tactic:
exact huv (hx.2 _ hadj ▸ (hx.2 _ hadj').symm)

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huv : v ≠ w
hadj : M.Adj u v
hadj' : M.Adj u w
⊢ False

Tactic:
obtain ⟨x, hx⟩ := hM (M.edge_vert hadj)

Result:
case intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huv : v ≠ w
hadj : M.Adj u v
hadj' : M.Adj u w
x : V
hx : (fun w => M.Adj u w) x ∧ ∀ (y : V), (fun w => M.Adj u w) y → y = x
⊢ False
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingsBefore_zero : upcrossingsBefore a b f 0 ω = 0

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0

Tactic:
simp [upcrossingsBefore]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- `castSucc` commutes with `predAbove`. -/
@[simp] lemma castSucc_predAbove_castSucc {n : ℕ} (a : Fin n) (b : Fin (n + 1)) :
    a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Proof state:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h,
  castSucc_pred_eq_pred_castSucc]

Result:
no goals

Proof state:
case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]

Result:
no goals

Proof state:
n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
obtain h | h := a.castSucc.lt_or_le b

Result:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
-- Mathlib/Data/Multiset/Bind.lean
theorem coe_bind (l : List α) (f : α → List β) : (@bind α β l fun a => f a) = l.flatMap f

Proof state:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a => ↑(f a)) = (↑(List.map (ofList ∘ f) l)).join

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a => ↑(f a)) = ↑(List.flatMap f l)

Tactic:
rw [List.flatMap, ← coe_join, List.map_map]

Result:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a => ↑(f a)) = (↑(List.map (ofList ∘ f) l)).join
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_const_smul (hp : p ≠ 0) {c : 𝕜} (f : lp E p) : ‖c • f‖ = ‖c‖ * ‖f‖

Proof state:
case inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖

Tactic:
have := mul_le_mul_of_nonneg_left (norm_const_smul_le hp c⁻¹ (c • f)) (norm_nonneg c)

Result:
case inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖

Proof state:
case inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖

Tactic:
rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
⊢ ‖c • f‖ = ‖c‖ * ‖f‖

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
f : ↥(lp E p)
⊢ ‖0 • f‖ = ‖0‖ * ‖f‖

case inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c • f‖ = ‖c‖ * ‖f‖

Proof state:
case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
f : ↥(lp E p)
⊢ ‖0 • f‖ = ‖0‖ * ‖f‖

Tactic:
simp

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c • f‖ = ‖c‖ * ‖f‖

Tactic:
refine le_antisymm (norm_const_smul_le hp c f) ?_

Result:
case inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_uIcc : (fun x => x - a) '' [[b, c]] = [[b - a, c - a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' [[b, c]] = [[b - a, c - a]]

Tactic:
simp [sub_eq_add_neg, add_comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_im (x : E) : im ⟪x, x⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ im ⟪x, x⟫_𝕜 = 0

Tactic:
rw [← @ofReal_inj 𝕜, im_eq_conj_sub]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ I * ((starRingEnd 𝕜) ⟪x, x⟫_𝕜 - ⟪x, x⟫_𝕜) / 2 = ↑0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ I * ((starRingEnd 𝕜) ⟪x, x⟫_𝕜 - ⟪x, x⟫_𝕜) / 2 = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem isOrdinal_not_mem_univ : IsOrdinal ∉ Class.univ.{u}

Proof state:
x : ZFSet.{u}
hx : ↑x = IsOrdinal
this : x.IsOrdinal
⊢ ↑x ∈ ↑x

Tactic:
rwa [Class.coe_mem, hx]

Result:
no goals

Proof state:
case intro.intro
x : ZFSet.{u}
hx : ↑x = IsOrdinal
⊢ x.IsOrdinal

Tactic:
refine ⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩ <;> rw [← Class.coe_apply, hx] at *

Result:
case intro.intro.refine_1
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y : ZFSet.{u}
hy : y.IsOrdinal
z : ZFSet.{u}
hz : ↑y z
⊢ z.IsOrdinal

case intro.intro.refine_2
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : ↑z✝ y✝
hzw : ↑w✝ z✝
hwx : w✝.IsOrdinal
⊢ ↑w✝ y✝

Proof state:
case intro.intro.refine_1
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y : ZFSet.{u}
hy : y.IsOrdinal
z : ZFSet.{u}
hz : ↑y z
⊢ z.IsOrdinal

case intro.intro.refine_2
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : ↑z✝ y✝
hzw : ↑w✝ z✝
hwx : w✝.IsOrdinal
⊢ ↑w✝ y✝

Tactic:
exacts [hy.mem hz, hwx.mem_trans hyz hzw]

Result:
no goals

Proof state:
case intro.intro
x : ZFSet.{u}
hx : ↑x = IsOrdinal
⊢ False

Tactic:
suffices IsOrdinal x by
  apply Class.mem_irrefl x
  rwa [Class.coe_mem, hx]

Result:
case intro.intro
x : ZFSet.{u}
hx : ↑x = IsOrdinal
⊢ x.IsOrdinal

Proof state:
x : ZFSet.{u}
hx : ↑x = IsOrdinal
this : x.IsOrdinal
⊢ False

Tactic:
apply Class.mem_irrefl x

Result:
x : ZFSet.{u}
hx : ↑x = IsOrdinal
this : x.IsOrdinal
⊢ ↑x ∈ ↑x

Proof state:
⊢ IsOrdinal ∉ Class.univ

Tactic:
rintro ⟨x, hx, -⟩

Result:
case intro.intro
x : ZFSet.{u}
hx : ↑x = IsOrdinal
⊢ False
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_intCast_mul {n : ℤ} {f : R[X]} : derivative ((n : R[X]) * f) =
    n * derivative f

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
f : R[X]
⊢ derivative (↑n * f) = ↑n * derivative f

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma of_openCover (H : ∀ i, P (𝒰.pullbackHom f i)) : P f

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ P f

Tactic:
apply of_iSup_eq_top (fun i ↦ (𝒰.map i).opensRange) 𝒰.iSup_opensRange

Result:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ ∀ (i : 𝒰.J), P (f ∣_ Scheme.Hom.opensRange (𝒰.map i))

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ ∀ (i : 𝒰.J), P (f ∣_ Scheme.Hom.opensRange (𝒰.map i))

Tactic:
exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (H i)

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma finite_quotient_of_finite_quotient_of_index_ne_zero {X : Type*} [MulAction G X]
    [Finite <| MulAction.orbitRel.Quotient G X] (hi : H.index ≠ 0) :
    Finite <| MulAction.orbitRel.Quotient H X

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : Finite (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
have := fintypeOfIndexNeZero hi

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : Finite (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
this : Fintype (G ⧸ H)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : Finite (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
this : Fintype (G ⧸ H)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
exact MulAction.finite_quotient_of_finite_quotient_of_finite_quotient

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem add_lt_add {x y z t : EReal} (h1 : x < y) (h2 : z < t) : x + z < y + t

Proof state:
case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t

Tactic:
lift x to ℝ using ⟨h1.ne_top, hx⟩

Result:
case inr.intro
y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + z < y + t

Proof state:
case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t

Tactic:
simp [h1, bot_le.trans_lt h2]

Result:
no goals

Proof state:
case inr.intro
y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + z < y + t

Tactic:
calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
_ ≤ y + t := add_le_add_right h1.le _

Result:
no goals

Proof state:
x y z t : EReal
h1 : x < y
h2 : z < t
⊢ x + z < y + t

Tactic:
rcases eq_or_ne x ⊥ with (rfl | hx)

Result:
case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t

case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t