harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LocalProperties/Basic.lean
theorem RingHom.HoldsForLocalizationAway.of_bijective
    (H : RingHom.HoldsForLocalizationAway P) (hf : Function.Bijective f) :
    P f

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
this✝ : Algebra R S := f.toAlgebra
this : IsLocalization (Submonoid.powers 1) R
⊢ P f

Tactic:
have := IsLocalization.isLocalization_of_algEquiv (.powers (1 : R))
  (AlgEquiv.ofBijective (Algebra.ofId R S) hf)

Result:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
this✝¹ : Algebra R S := f.toAlgebra
this✝ : IsLocalization (Submonoid.powers 1) R
this : IsLocalization (Submonoid.powers 1) S
⊢ P f

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
⊢ P f

Tactic:
letI := f.toAlgebra

Result:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
this : Algebra R S := f.toAlgebra
⊢ P f

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
this✝¹ : Algebra R S := f.toAlgebra
this✝ : IsLocalization (Submonoid.powers 1) R
this : IsLocalization (Submonoid.powers 1) S
⊢ P f

Tactic:
exact H _ 1

Result:
no goals

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
this : Algebra R S := f.toAlgebra
⊢ P f

Tactic:
have := IsLocalization.at_units (.powers (1 : R)) (by simp)

Result:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
this✝ : Algebra R S := f.toAlgebra
this : IsLocalization (Submonoid.powers 1) R
⊢ P f

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
hf : Function.Bijective ⇑f
this : Algebra R S := f.toAlgebra
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid R

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
@[simp]
lemma valMinAbs_eq_zero (x : ZMod n) : x.valMinAbs = 0 ↔ x = 0

Proof state:
case zero
x : ZMod 0
⊢ x.valMinAbs = 0 ↔ x = 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
x : ZMod n
⊢ x.valMinAbs = 0 ↔ x = 0

Tactic:
rcases n with - | n

Result:
case zero
x : ZMod 0
⊢ x.valMinAbs = 0 ↔ x = 0

case succ
n : ℕ
x : ZMod (n + 1)
⊢ x.valMinAbs = 0 ↔ x = 0

Proof state:
case succ
n : ℕ
x : ZMod (n + 1)
⊢ x.valMinAbs = 0 ↔ x = 0

Tactic:
rw [← valMinAbs_zero n.succ]

Result:
case succ
n : ℕ
x : ZMod (n + 1)
⊢ x.valMinAbs = valMinAbs 0 ↔ x = 0

Proof state:
case succ
n : ℕ
x : ZMod (n + 1)
⊢ x.valMinAbs = valMinAbs 0 ↔ x = 0

Tactic:
apply injective_valMinAbs.eq_iff

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_left_comm : s ○ (t ○ u) = t ○ (s ○ u)

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u : Finset α
⊢ s ○ (t ○ u) = t ○ (s ○ u)

Tactic:
simp_rw [← disjSups_assoc, disjSups_comm s]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem diagonalHomEquiv_symm_partialProd_succ (f : (Fin n → G) → A) (g : Fin (n + 1) → G)
    (a : Fin (n + 1)) :
    ((diagonalHomEquiv n A).symm f).hom (Finsupp.single (Fin.partialProd g ∘ a.succ.succAbove) 1)
      = f (Fin.contractNth a (· * ·) g)

Proof state:
case e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
a : Fin (n + 1)
x✝ : Fin n
⊢ (Fin.partialProd g (a.succ.succAbove x✝.castSucc))⁻¹ *
      (Fin.partialProd g (a.succAbove x✝).castSucc * g (a.succAbove x✝)) =
    a.contractNth (fun x1 x2 => x1 * x2) g x✝

Tactic:
rw [← Fin.partialProd_succ, Fin.inv_partialProd_mul_eq_contractNth]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
a : Fin (n + 1)
⊢ (f fun i =>
      (Fin.partialProd g (a.succ.succAbove i.castSucc))⁻¹ *
        (Fin.partialProd g (a.succAbove i).castSucc * g (a.succAbove i))) =
    f (a.contractNth (fun x1 x2 => x1 * x2) g)

Tactic:
congr

Result:
case e_a
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
a : Fin (n + 1)
⊢ (fun i =>
      (Fin.partialProd g (a.succ.succAbove i.castSucc))⁻¹ *
        (Fin.partialProd g (a.succAbove i).castSucc * g (a.succAbove i))) =
    a.contractNth (fun x1 x2 => x1 * x2) g

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
a : Fin (n + 1)
⊢ (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom) (single (Fin.partialProd g ∘ a.succ.succAbove) 1) =
    f (a.contractNth (fun x1 x2 => x1 * x2) g)

Tactic:
simp only [diagonalHomEquiv_symm_apply, Function.comp_apply, Fin.succ_succAbove_zero,
  Fin.partialProd_zero, map_one, Fin.succ_succAbove_succ, LinearMap.one_apply,
  Fin.partialProd_succ]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
a : Fin (n + 1)
⊢ (f fun i =>
      (Fin.partialProd g (a.succ.succAbove i.castSucc))⁻¹ *
        (Fin.partialProd g (a.succAbove i).castSucc * g (a.succAbove i))) =
    f (a.contractNth (fun x1 x2 => x1 * x2) g)

Proof state:
case e_a
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
a : Fin (n + 1)
⊢ (fun i =>
      (Fin.partialProd g (a.succ.succAbove i.castSucc))⁻¹ *
        (Fin.partialProd g (a.succAbove i).castSucc * g (a.succAbove i))) =
    a.contractNth (fun x1 x2 => x1 * x2) g

Tactic:
ext

Result:
case e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
a : Fin (n + 1)
x✝ : Fin n
⊢ (Fin.partialProd g (a.succ.succAbove x✝.castSucc))⁻¹ *
      (Fin.partialProd g (a.succAbove x✝).castSucc * g (a.succAbove x✝)) =
    a.contractNth (fun x1 x2 => x1 * x2) g x✝
-- Mathlib/Logic/Basic.lean
theorem ite_ne_left_iff : ite P a b ≠ a ↔ ¬P ∧ a ≠ b :=
  dite_ne_left_iff.trans <| by rw [exists_prop]

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b

Tactic:
rw [exists_prop]

Result:
no goals
-- Mathlib/Logic/Unique.lean
theorem unique_iff_subsingleton_and_nonempty (α : Sort u) :
    Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α :=
  ⟨fun ⟨u⟩ ↦ by constructor <;> exact inferInstance,
   fun ⟨hs, hn⟩ ↦ nonempty_unique α⟩

Proof state:
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α

Tactic:
constructor <;> exact inferInstance

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem fderiv_comp_deriv_of_eq (hl : DifferentiableAt 𝕜 l y) (hf : DifferentiableAt 𝕜 f x)
    (hy : y = f x) :
    deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l y
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)

Tactic:
rw [hy] at hl

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l (f x)
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l (f x)
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)

Tactic:
exact fderiv_comp_deriv x hl hf

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma ediv_two_mul_two_add_one_of_odd : Odd n → n / 2 * 2 + 1 = n

Proof state:
case h.e'_2.h.e'_6
c : ℤ
⊢ 1 = (2 * c + 1) % 2

Tactic:
simp [Int.add_emod]

Result:
no goals

Proof state:
n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n

Tactic:
rintro ⟨c, rfl⟩

Result:
case intro
c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1

Proof state:
case intro
c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1

Tactic:
convert Int.ediv_add_emod' (2 * c + 1) 2

Result:
case h.e'_2.h.e'_6
c : ℤ
⊢ 1 = (2 * c + 1) % 2
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_congr' {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) :
    Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Tactic:
rw [Tendsto, Tendsto, map_congr hl]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_le_average_pos (hμ : μ ≠ 0) (hf : Integrable f μ) :
    0 < μ {x | f x ≤ ⨍ a, f a ∂μ}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ 0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}

Tactic:
simpa using measure_le_setAverage_pos (Measure.measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)
  hf.integrableOn

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_le_count_map [DecidableEq β] (l : List α) (f : α → β) (x : α) :
    count x l ≤ count (f x) (map f l)

Proof state:
case h
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ ∀ (x_1 : α), x_1 ∈ l → (x_1 == x) = true → ((fun x_2 => x_2 == f x) ∘ f) x_1 = true

Tactic:
simp +contextual

Result:
no goals

Proof state:
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ countP (fun x_1 => x_1 == x) l ≤ countP ((fun x_1 => x_1 == f x) ∘ f) l

Tactic:
apply countP_mono_left

Result:
case h
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ ∀ (x_1 : α), x_1 ∈ l → (x_1 == x) = true → ((fun x_2 => x_2 == f x) ∘ f) x_1 = true

Proof state:
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ count x l ≤ count (f x) (map f l)

Tactic:
rw [count, count, countP_map]

Result:
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ countP (fun x_1 => x_1 == x) l ≤ countP ((fun x_1 => x_1 == f x) ∘ f) l
-- Mathlib/Analysis/Calculus/LogDeriv.lean
theorem logDeriv_comp {f : 𝕜' → 𝕜'} {g : 𝕜 → 𝕜'} {x : 𝕜} (hf : DifferentiableAt 𝕜' f (g x))
    (hg : DifferentiableAt 𝕜 g x) : logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ deriv f (g x) * deriv g x / f (g x) = deriv f (g x) / f (g x) * deriv g x

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x

Tactic:
simp only [logDeriv, Pi.div_apply, deriv_comp _ hf hg, comp_apply]

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ deriv f (g x) * deriv g x / f (g x) = deriv f (g x) / f (g x) * deriv g x
-- Mathlib/RingTheory/Localization/Cardinality.lean
theorem cardinalMk (L : Type u) [CommRing L] [Algebra R L]
    (S : Submonoid R) [IsLocalization S L] (hS : S ≤ R⁰) : #L = #R

Proof state:
R : Type u
inst✝³ : CommRing R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
⊢ #L = #R

Tactic:
simpa using lift_cardinalMk L S hS

Result:
no goals
-- Mathlib/Order/ModularLattice.lean
theorem inf_covBy_of_covBy_sup_right : b ⋖ a ⊔ b → a ⊓ b ⋖ a

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ b ⊔ a → b ⊓ a ⋖ a

Tactic:
exact inf_covBy_of_covBy_sup_left

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ a ⊔ b → a ⊓ b ⋖ a

Tactic:
rw [inf_comm, sup_comm]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ b ⊔ a → b ⊓ a ⋖ a
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_right`. -/
lemma mul_div_mul_right_le (h : 0 ≤ a / b) : a * c / (b * c) ≤ a / b

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : 0 ≤ a / b
hc : c ≠ 0
⊢ a * c / (b * c) ≤ a / b

Tactic:
rw [mul_div_mul_right _ _ hc]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : 0 ≤ a / b
⊢ a * 0 / (b * 0) ≤ a / b

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : 0 ≤ a / b
⊢ a * c / (b * c) ≤ a / b

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : 0 ≤ a / b
⊢ a * 0 / (b * 0) ≤ a / b

case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : 0 ≤ a / b
hc : c ≠ 0
⊢ a * c / (b * c) ≤ a / b
-- Mathlib/Data/Set/Lattice.lean
lemma exists_sUnion {S : Set (Set α)} {p : α → Prop} :
    (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x

Proof state:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x

Tactic:
simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem ker.incl_comp_lift (h : g.comp f = 0) : (incl g.ker).comp (ker.lift f g h) = f

Proof state:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
⊢ (incl g.ker).comp (lift f g h) = f

Tactic:
ext

Result:
case H
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
x✝ : V₁
⊢ ((incl g.ker).comp (lift f g h)) x✝ = f x✝

Proof state:
case H
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
x✝ : V₁
⊢ ((incl g.ker).comp (lift f g h)) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/CompleteField.lean
theorem coe_lt_inducedMap_iff : (q : β) < inducedMap α β a ↔ (q : α) < a

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap α β a ↔ ↑q < a

Tactic:
refine ⟨fun h => ?_, fun hq => ?_⟩

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a

case refine_2
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a

Tactic:
rw [← inducedMap_rat α] at h

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
h : inducedMap α β ↑q < inducedMap α β a
⊢ ↑q < a

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq

Result:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < inducedMap α β a

Proof state:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < inducedMap α β a

Tactic:
apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)

Result:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < ↑q'

Proof state:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < ↑q'

Tactic:
exact mod_cast hq

Result:
no goals

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
h : inducedMap α β ↑q < inducedMap α β a
⊢ ↑q < a

Tactic:
exact (inducedMap_mono α β).reflect_lt h

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem _root_.sSupHom.apply_blimsup_le [CompleteLattice γ] (g : sSupHom α γ) :
    g (blimsup u f p) ≤ blimsup (g ∘ u) f p

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ g (⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)

Tactic:
refine ((OrderHomClass.mono g).map_iInf₂_le _).trans ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ⨅ i ∈ f, g (⨆ b, ⨆ (_ : p b ∧ b ∈ i), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ⨅ i ∈ f, g (⨆ b, ⨆ (_ : p b ∧ b ∈ i), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)

Tactic:
simp only [_root_.map_iSup, le_refl]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ g (blimsup u f p) ≤ blimsup (⇑g ∘ u) f p

Tactic:
simp only [blimsup_eq_iInf_biSup, Function.comp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ g (⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)
-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
theorem ContDiffAt.iteratedFDeriv_comp_perm
    (h : ContDiffAt 𝕜 ω f x) {n : ℕ} (v : Fin n → E) (σ : Perm (Fin n)) :
    iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f univ x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f univ x) v

Tactic:
exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

Tactic:
rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f univ x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f univ x) v
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem one_braiding {X Y : Mon_ C} : (X ⊗ Y).one ≫ (β_ X.X Y.X).hom = (Y ⊗ X).one

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Mon_ C
⊢ (ρ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).inv ≫ (Y.one ⊗ X.one) = Y.one ⊗ X.one

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Mon_ C
⊢ (X ⊗ Y).one ≫ (β_ X.X Y.X).hom = (Y ⊗ X).one

Tactic:
simp only [monMonoidalStruct_tensorObj_X, tensor_one, Category.assoc,
  BraidedCategory.braiding_naturality, braiding_tensorUnit_right, Iso.cancel_iso_inv_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Mon_ C
⊢ (ρ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).inv ≫ (Y.one ⊗ X.one) = Y.one ⊗ X.one