harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
@[simp]
lemma autMap_comp {X Y Z : C} [IsConnected X] [IsGalois Y] [IsGalois Z] (f : X ⟶ Y)
    (g : Y ⟶ Z) : autMap (f ≫ g) = autMap g ∘ autMap f

Proof state:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ autMap (f ≫ g) = autMap g ∘ autMap f

Tactic:
refine funext fun σ ↦ autMap_unique _ σ _ ?_

Result:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g

Proof state:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g

Tactic:
rw [Function.comp_apply, Category.assoc, comp_autMap, ← Category.assoc]

Result:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ (autMap f σ).hom) ≫ g = σ.hom ≫ f ≫ g

Proof state:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ (autMap f σ).hom) ≫ g = σ.hom ≫ f ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem one_left (b : ℕ) : J(1 | b) = 1 :=
  List.prod_eq_one fun z hz => by
    let ⟨p, hp, he⟩ := List.mem_pmap.1 hz
    -- Porting note: The line 150 was added because Lean does not synthesize the instance
    -- `[Fact (Nat.Prime p)]` automatically (it is needed for `legendreSym.at_one`)
    letI : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩
    rw [← he, legendreSym.at_one]

Proof state:
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯
⊢ z = 1

Tactic:
let ⟨p, hp, he⟩ := List.mem_pmap.1 hz

Result:
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
⊢ z = 1

Proof state:
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
this : Fact (Nat.Prime p) := { out := prime_of_mem_primeFactorsList hp }
⊢ z = 1

Tactic:
rw [← he, legendreSym.at_one]

Result:
no goals

Proof state:
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
⊢ z = 1

Tactic:
letI : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩

Result:
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
this : Fact (Nat.Prime p) := { out := prime_of_mem_primeFactorsList hp }
⊢ z = 1
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem le_one_of_mul_le_left [MulRightReflectLE α] {a b : α}
    (h : a * b ≤ b) :
    a ≤ 1 :=
  le_of_mul_le_mul_right' (a := b) <| by simpa only [one_mul]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulRightReflectLE α
a b : α
h : a * b ≤ b
⊢ a * b ≤ 1 * b

Tactic:
simpa only [one_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_mem_Ioc (z : ℂ) : arg z ∈ Set.Ioc (-π) π

Proof state:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
have hπ : 0 < π := Real.pi_pos

Result:
z : ℂ
hπ : 0 < π
⊢ z.arg ∈ Ioc (-π) π

Proof state:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]

Result:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Proof state:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos ↑(z.arg + ↑N * (2 * π)) + sin ↑(z.arg + ↑N * (2 * π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Tactic:
push_cast at this

Result:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Proof state:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Tactic:
have := arg_mul_cos_add_sin_mul_I (norm_pos_iff.mpr hz) hN

Result:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos ↑(z.arg + ↑N * (2 * π)) + sin ↑(z.arg + ↑N * (2 * π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Proof state:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Tactic:
rwa [this]

Result:
no goals

Proof state:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩

Result:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ z.arg ∈ Ioc (-π) π

Proof state:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN

Result:
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Proof state:
z : ℂ
hπ : 0 < π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rcases eq_or_ne z 0 with (rfl | hz)

Result:
case inl
hπ : 0 < π
⊢ arg 0 ∈ Ioc (-π) π

case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ z.arg ∈ Ioc (-π) π

Proof state:
case inl
hπ : 0 < π
⊢ arg 0 ∈ Ioc (-π) π

Tactic:
simp [hπ, hπ.le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
    {f : Option β → Option β} (h : m.WF) : (Const.alter m k f).getKey! k' =
      if k == k' then
        if (f (Const.get? m k)).isSome then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).getKey! k' =
    if (k == k') = true then if (f (get? m k)).isSome = true then k else default else m.getKey! k'

Tactic:
simp_to_raw using Raw₀.Const.getKey!_alter

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
    map f (filter p as) = foldr (fun a bs => bif p a then f a :: bs else bs) [] as

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
as : List α
⊢ map f (filter p as) = foldr (fun a bs => bif p a then f a :: bs else bs) [] as

Tactic:
induction as with
| nil => rfl
| cons head _ ih =>
  simp only [foldr]
  cases hp : p head <;> simp [filter, *]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
head : α
tail✝ : List α
ih : map f (filter p tail✝) = foldr (fun a bs => bif p a then f a :: bs else bs) [] tail✝
⊢ map f (filter p (head :: tail✝)) =
    bif p head then f head :: foldr (fun a bs => bif p a then f a :: bs else bs) [] tail✝
    else foldr (fun a bs => bif p a then f a :: bs else bs) [] tail✝

Tactic:
cases hp : p head <;> simp [filter, *]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
head : α
tail✝ : List α
ih : map f (filter p tail✝) = foldr (fun a bs => bif p a then f a :: bs else bs) [] tail✝
⊢ map f (filter p (head :: tail✝)) = foldr (fun a bs => bif p a then f a :: bs else bs) [] (head :: tail✝)

Tactic:
simp only [foldr]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
head : α
tail✝ : List α
ih : map f (filter p tail✝) = foldr (fun a bs => bif p a then f a :: bs else bs) [] tail✝
⊢ map f (filter p (head :: tail✝)) =
    bif p head then f head :: foldr (fun a bs => bif p a then f a :: bs else bs) [] tail✝
    else foldr (fun a bs => bif p a then f a :: bs else bs) [] tail✝

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
⊢ map f (filter p []) = foldr (fun a bs => bif p a then f a :: bs else bs) [] []

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
lemma hom_bijective {M N : ModuleCat.{v} R} :
    Function.Bijective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) where
  left f g h

Proof state:
case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g

Tactic:
cases g

Result:
case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk._private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
hom'✝¹ hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝¹ }.hom = { hom' := hom'✝ }.hom
⊢ { hom' := hom'✝¹ } = { hom' := hom'✝ }

Proof state:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Result:
case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g

Proof state:
case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk._private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
hom'✝¹ hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝¹ }.hom = { hom' := hom'✝ }.hom
⊢ { hom' := hom'✝¹ } = { hom' := hom'✝ }

Tactic:
simpa using h

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_b₈ : (W.variableChange C).b₈ = C.u⁻¹ ^ 8 *
    (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (W.variableChange C).b₈ = ↑C.u⁻¹ ^ 8 * (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4)

Tactic:
simp only [b₂, b₄, b₆, b₈, variableChange_a₁, variableChange_a₂, variableChange_a₃,
  variableChange_a₄, variableChange_a₆]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 *
              (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) +
            4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) *
              (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) -
          ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) *
            (↑C.u⁻¹ ^ 4 *
              (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
        ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 -
      (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) ^ 2 =
    ↑C.u⁻¹ ^ 8 *
      (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 +
              3 * C.r * (W.a₃ ^ 2 + 4 * W.a₆) +
            3 * C.r ^ 2 * (2 * W.a₄ + W.a₁ * W.a₃) +
          C.r ^ 3 * (W.a₁ ^ 2 + 4 * W.a₂) +
        3 * C.r ^ 4)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 *
              (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) +
            4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) *
              (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) -
          ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) *
            (↑C.u⁻¹ ^ 4 *
              (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
        ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 -
      (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) ^ 2 =
    ↑C.u⁻¹ ^ 8 *
      (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 +
              3 * C.r * (W.a₃ ^ 2 + 4 * W.a₆) +
            3 * C.r ^ 2 * (2 * W.a₄ + W.a₁ * W.a₃) +
          C.r ^ 3 * (W.a₁ ^ 2 + 4 * W.a₂) +
        3 * C.r ^ 4)

Tactic:
ring1

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem ContinuousLinearMap.comp_analyticOnNhd
    {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOnNhd 𝕜 f s) :
    AnalyticOnNhd 𝕜 (g ∘ f) s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (⇑g ∘ f) s

Tactic:
rintro x hx

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
x : E
hx : x ∈ s
⊢ AnalyticAt 𝕜 (⇑g ∘ f) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
x : E
hx : x ∈ s
⊢ AnalyticAt 𝕜 (⇑g ∘ f) x

Tactic:
rcases h x hx with ⟨p, r, hp⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (⇑g ∘ f) x

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (⇑g ∘ f) x

Tactic:
exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.subtypePerm (hf : f.IsCycleOn s) :
    (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycleOn _root_.Set.univ

Proof state:
case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
haveI := hs.coe_sort

Result:
case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
this : Subsingleton ↑s
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Proof state:
case h.e'_3
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | (f.subtypePerm ⋯) x ≠ x}

Tactic:
exact fun x => ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs x.2)

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
obtain hs | hs := s.subsingleton_or_nontrivial

Result:
case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

case inr
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Proof state:
case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
this : Subsingleton ↑s
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
exact isCycleOn_of_subsingleton _ _

Result:
no goals

Proof state:
case h.e'_3
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ _root_.Set.univ = {x | (f.subtypePerm ⋯) x ≠ x}

Tactic:
rw [eq_comm, Set.eq_univ_iff_forall]

Result:
case h.e'_3
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | (f.subtypePerm ⋯) x ≠ x}

Proof state:
case inr
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
convert (hf.isCycle_subtypePerm hs).isCycleOn

Result:
case h.e'_3
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ _root_.Set.univ = {x | (f.subtypePerm ⋯) x ≠ x}
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLin_finTwoProd_apply (a b c d : R) (x : R × R) :
    Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R) !![a, b; c, d] x =
      (a * x.fst + b * x.snd, c * x.fst + d * x.snd)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b c d : R
x : R × R
⊢ ((toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) !![a, b; c, d]) x = (a * x.1 + b * x.2, c * x.1 + d * x.2)

Tactic:
simp [Matrix.toLin_apply, Matrix.mulVec, dotProduct]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_iff_isIso_descOpcycles (φ : S₁ ⟶ S₂)
    (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
    QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero]))

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.f ≫ φ.τ₂ = 0

Tactic:
rw [← φ.comm₁₂, hf₂, comp_zero]

Result:
no goals

Proof state:
C : Type ?u.31732
inst✝⁵ : Category.{?u.31736, ?u.31732} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.f ≫ φ.τ₂ = 0

Tactic:
rw [← φ.comm₁₂, hf₂, comp_zero]

Result:
no goals

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
H : RightHomologyMapData φ
  (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ (CokernelCofork.ofπ S₁.pOpcycles ⋯) S₁.opcyclesIsCokernel)
  (RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
  { φQ := S₁.descOpcycles φ.τ₂ ⋯, φH := S₁.descOpcycles φ.τ₂ ⋯, commp := ⋯, commg' := ⋯, commι := ⋯ }
⊢ QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)

Tactic:
exact H.quasiIso_iff

Result:
no goals

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)

Tactic:
let H : RightHomologyMapData φ
    (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ _ S₁.opcyclesIsCokernel)
      (RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
  { φQ := S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero])
    φH := S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero]) }

Result:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
H : RightHomologyMapData φ
  (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ (CokernelCofork.ofπ S₁.pOpcycles ⋯) S₁.opcyclesIsCokernel)
  (RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
  { φQ := S₁.descOpcycles φ.τ₂ ⋯, φH := S₁.descOpcycles φ.τ₂ ⋯, commp := ⋯, commg' := ⋯, commι := ⋯ }
⊢ QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_const_lintegral (c : ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) :
    ((const α c).restrict s).lintegral μ = c * μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((const α c).restrict s).lintegral μ = c * μ s

Tactic:
rw [restrict_lintegral_eq_lintegral_restrict _ hs, const_lintegral_restrict]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_submatrix_sum_swap_sum_swap {l m n o α : Type*} (A : Matrix n l α)
    (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
    (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A

Proof state:
l : Type u_14
m : Type u_15
n : Type u_16
o : Type u_17
α : Type u_18
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOn.mono {s' : Set α} (hf : UniformCauchySeqOn F p s) (hss' : s' ⊆ s) :
    UniformCauchySeqOn F p s'

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
s' : Set α
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')

Tactic:
exact hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
s' : Set α
hf : UniformCauchySeqOn F p s
hss' : s' ⊆ s
⊢ UniformCauchySeqOn F p s'

Tactic:
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
s' : Set α
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem eq_of_norm_add_lt_right {z1 z2 : ℚ_[p]} (h : ‖z1 + z2‖ < ‖z2‖) : ‖z1‖ = ‖z2‖ :=
  _root_.by_contradiction fun hne ↦
    not_lt_of_ge (by rw [padicNormE.add_eq_max_of_ne hne]; apply le_max_right) h

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z2‖

Tactic:
rw [padicNormE.add_eq_max_of_ne hne]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z2‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z2‖

Tactic:
apply le_max_right

Result:
no goals