harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Unramified/Basic.lean
theorem of_comp [FormallyUnramified R B] : FormallyUnramified A B

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
x : B
⊢ (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₁) x) = (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₂) x)

Tactic:
exact AlgHom.congr_fun e' x

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem sumCasesOn_right {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ →. σ} (hf : Computable f)
    (hg : Computable₂ g) (hh : Partrec₂ h) :
    @Partrec _ σ _ _ fun a => Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a) :=
  have :
    Partrec fun a =>
      (Option.casesOn (Sum.casesOn (f a) (fun _ => Option.none) Option.some : Option γ)
          (some (Sum.casesOn (f a) (fun b => some (g a b)) fun _ => Option.none)) fun c =>
          (h a c).map Option.some :
        Part (Option σ)) :=
    optionCasesOn_right (g := fun a n => Part.map Option.some (h a n))
      (sumCasesOn hf (const Option.none).to₂ (option_some.comp snd).to₂)
      (sumCasesOn (g := fun a n => Option.some (g a n)) hf (option_some.comp hg)
        (const Option.none).to₂)
      (option_some_iff.2 hh)
  option_some_iff.1 <| this.of_eq fun a => by cases f a <;> simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a =>
    Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)
a : α
⊢ (Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a))

Tactic:
cases f a <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashSet/RawLemmas.lean
theorem ext {m m' : Raw α} : m.inner = m'.inner → m = m'

Proof state:
case mk.mk
α : Type u
inner✝¹ inner✝ : HashMap.Raw α Unit
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }

Tactic:
rintro rfl

Result:
case mk.mk
α : Type u
inner✝ : HashMap.Raw α Unit
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }

Proof state:
α : Type u
m m' : Raw α
⊢ m.inner = m'.inner → m = m'

Tactic:
cases m

Result:
case mk
α : Type u
m' : Raw α
inner✝ : HashMap.Raw α Unit
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Proof state:
case mk.mk
α : Type u
inner✝ : HashMap.Raw α Unit
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }

Tactic:
rfl

Result:
no goals

Proof state:
case mk
α : Type u
m' : Raw α
inner✝ : HashMap.Raw α Unit
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Tactic:
cases m'

Result:
case mk.mk
α : Type u
inner✝¹ inner✝ : HashMap.Raw α Unit
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }
-- Mathlib/CategoryTheory/MorphismProperty/Composition.lean
/-- The multiplicative closure of `W` is the smallest multiplicative property greater than or equal
to `W`. -/
@[simp]
lemma multiplicativeClosure_le_iff (W' : MorphismProperty C) [W'.IsMultiplicative] :
    multiplicativeClosure W ≤ W' ↔ W ≤ W' where
  mp h := le_multiplicativeClosure W |>.trans h
  mpr h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
⊢ W.multiplicativeClosure ≤ W'

Tactic:
intro _ _ _ hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W' f✝

Proof state:
case id
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x : C
⊢ W' (𝟙 x)

Tactic:
exact W'.id_mem _

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W' f✝

Tactic:
induction hf with
| of _ hf => exact h _ hf
| id x => exact W'.id_mem _
| comp_of _ _ _ hg hf => exact W'.comp_mem _ _ hf (h _ hg)

Result:
no goals

Proof state:
case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : W.multiplicativeClosure f✝
hg : W g✝
hf : W' f✝
⊢ W' (f✝ ≫ g✝)

Tactic:
exact W'.comp_mem _ _ hf (h _ hg)

Result:
no goals

Proof state:
case of
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
hf : W f✝
⊢ W' f✝

Tactic:
exact h _ hf

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isClique_map_image_iff {f : α ↪ β} :
    (G.map f).IsClique (f '' s) ↔ G.IsClique s

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ (SimpleGraph.map f G).IsClique (⇑f '' s) ↔ G.IsClique s

Tactic:
rw [isClique_map_iff, f.injective.subsingleton_image_iff]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Proof state:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Subsingleton
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Tactic:
simp [hs, IsClique.of_subsingleton]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Nontrivial
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Tactic:
simp [or_iff_right hs.not_subsingleton, Set.image_eq_image f.injective]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Tactic:
obtain (hs | hs) := s.subsingleton_or_nontrivial

Result:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Subsingleton
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Nontrivial
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem lengthParity_eq_ofAdd_length (w : W) :
    cs.lengthParity w = Multiplicative.ofAdd (↑(ℓ w))

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.lengthParity w = Multiplicative.ofAdd ↑(cs.length w)

Tactic:
rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : ω.length = cs.length (cs.wordProd ω)
⊢ cs.lengthParity (cs.wordProd ω) = Multiplicative.ofAdd ↑(cs.length (cs.wordProd ω))

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : ω.length = cs.length (cs.wordProd ω)
⊢ cs.lengthParity (cs.wordProd ω) = Multiplicative.ofAdd ↑(cs.length (cs.wordProd ω))

Tactic:
rw [← hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
  prod_replicate, ← ofAdd_nsmul, nsmul_one]

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
lemma add_one_natCast_le_withTop_of_lt {m : ℕ} {n : WithTop ℕ∞} (h : m < n) : (m + 1 : ℕ) ≤ n

Proof state:
m : ℕ
n✝ : WithTop ℕ∞
n : ℕ
h : ↑m < ↑n
⊢ ↑(m + 1) ≤ ↑n

Tactic:
simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h

Result:
no goals

Proof state:
m : ℕ
n : WithTop ℕ∞
h : ↑m < ⊤
⊢ ↑(m + 1) ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
m : ℕ
n : WithTop ℕ∞
h : ↑m < ↑⊤
⊢ ↑(m + 1) ≤ ↑⊤

Tactic:
exact WithTop.coe_le_coe.2 (OrderTop.le_top _)

Result:
no goals

Proof state:
m : ℕ
n : WithTop ℕ∞
h : ↑m < n
⊢ ↑(m + 1) ≤ n

Tactic:
match n with
| ⊤ => exact le_top
| (⊤ : ℕ∞) => exact WithTop.coe_le_coe.2 (OrderTop.le_top _)
| (n : ℕ) => simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_of_eq_div (h : a = c / b) : a * b = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a = c / b
⊢ a * b = c

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem tendstoUniformlyOn_iff {ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
    TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Proof state:
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Tactic:
refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩

Result:
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Proof state:
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩

Result:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_one : cramer (1 : Matrix n n α) = 1

Proof state:
case h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ (cramer 1 ∘ₗ LinearMap.single α (fun i => α) i) 1 j = (1 ∘ₗ LinearMap.single α (fun i => α) i) 1 j

Tactic:
convert congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j

Result:
case h.e'_3.h.e'_1
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ 1 = det 1

case h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ ∀ (j : n), Pi.single i 1 j = 1 j i

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
⊢ cramer 1 = 1

Tactic:
ext i j

Result:
case h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ (cramer 1 ∘ₗ LinearMap.single α (fun i => α) i) 1 j = (1 ∘ₗ LinearMap.single α (fun i => α) i) 1 j

Proof state:
case h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ ∀ (j : n), Pi.single i 1 j = 1 j i

Tactic:
intro j

Result:
case h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j✝ j : n
⊢ Pi.single i 1 j = 1 j i

Proof state:
case h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j✝ j : n
⊢ Pi.single i 1 j = 1 j i

Tactic:
rw [Matrix.one_eq_pi_single, Pi.single_comm]

Result:
no goals

Proof state:
case h.e'_3.h.e'_1
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ 1 = det 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem image_toPullbackDiag (f : X → Y) (s : Set X) :
    toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Proof state:
case h.mpr.mk.mk.intro
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
h : f (x, x).1 = f (x, x).2
h2x : ⟨(x, x), h⟩ ∈ Subtype.val ⁻¹' s ×ˢ s
⊢ ⟨(x, x), h⟩ ∈ toPullbackDiag f '' s

Tactic:
exact mem_image_of_mem _ h2x.1

Result:
no goals

Proof state:
case h.mp
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.mp.intro.intro
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
hx : x ∈ s
⊢ toPullbackDiag f x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Proof state:
case h
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
constructor

Result:
case h.mp
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

case h.mpr
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s

Proof state:
case h.mpr
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s

Tactic:
obtain ⟨⟨x, y⟩, h⟩ := x

Result:
case h.mpr.mk.mk
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x y : X
h : f (x, y).1 = f (x, y).2
⊢ ⟨(x, y), h⟩ ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s → ⟨(x, y), h⟩ ∈ toPullbackDiag f '' s

Proof state:
case h.mp.intro.intro
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
hx : x ∈ s
⊢ toPullbackDiag f x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
exact ⟨rfl, hx, hx⟩

Result:
no goals

Proof state:
case h.mpr.mk.mk
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x y : X
h : f (x, y).1 = f (x, y).2
⊢ ⟨(x, y), h⟩ ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s → ⟨(x, y), h⟩ ∈ toPullbackDiag f '' s

Tactic:
rintro ⟨rfl : x = y, h2x⟩

Result:
case h.mpr.mk.mk.intro
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
h : f (x, x).1 = f (x, x).2
h2x : ⟨(x, x), h⟩ ∈ Subtype.val ⁻¹' s ×ˢ s
⊢ ⟨(x, x), h⟩ ∈ toPullbackDiag f '' s

Proof state:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
⊢ toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
ext x

Result:
case h
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem HasProd.mul (hf : HasProd f a) (hg : HasProd g b) :
    HasProd (fun b ↦ f b * g b) (a * b)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
inst✝ : ContinuousMul α
hf : HasProd f a
hg : HasProd g b
⊢ HasProd (fun b => f b * g b) (a * b)

Tactic:
dsimp only [HasProd] at hf hg ⊢

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
inst✝ : ContinuousMul α
hf : Tendsto (fun s => ∏ b ∈ s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∏ b ∈ s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∏ b ∈ s, f b * g b) atTop (𝓝 (a * b))

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
inst✝ : ContinuousMul α
hf : Tendsto (fun s => ∏ b ∈ s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∏ b ∈ s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∏ b ∈ s, f b * g b) atTop (𝓝 (a * b))

Tactic:
simp_rw [prod_mul_distrib]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
inst✝ : ContinuousMul α
hf : Tendsto (fun s => ∏ b ∈ s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∏ b ∈ s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => (∏ x ∈ s, f x) * ∏ x ∈ s, g x) atTop (𝓝 (a * b))

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
inst✝ : ContinuousMul α
hf : Tendsto (fun s => ∏ b ∈ s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∏ b ∈ s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => (∏ x ∈ s, f x) * ∏ x ∈ s, g x) atTop (𝓝 (a * b))

Tactic:
exact hf.mul hg

Result:
no goals
-- Mathlib/RepresentationTheory/Maschke.lean
theorem exists_leftInverse_of_injective
    (f : V →ₗ[MonoidAlgebra k G] W) (hf : LinearMap.ker f = ⊥) :
    ∃ g : W →ₗ[MonoidAlgebra k G] V, g.comp f = LinearMap.id

Proof state:
case intro
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V
hφ : φ ∘ₗ ↑k f = LinearMap.id
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
refine ⟨φ.equivariantProjection G, DFunLike.ext _ _ ?_⟩

Result:
case intro
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V
hφ : φ ∘ₗ ↑k f = LinearMap.id
⊢ ∀ (x : V), (LinearMap.equivariantProjection G φ ∘ₗ f) x = LinearMap.id x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_set (a b : α) (as : Array α) (i : Nat) (h : i < as.size) :
    (as.set i a).set i b (by simpa using h) = as.set i b

Proof state:
α : Type ?u.126843
a b : α
as : Array α
i : Nat
h : i < as.size
⊢ i < (as.set i a h).size

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
a b : α
as : Array α
i : Nat
h : i < as.size
⊢ (as.set i a h).set i b ⋯ = as.set i b h

Tactic:
cases as

Result:
case mk
α : Type u_1
a b : α
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ ({ toList := toList✝ }.set i a h).set i b ⋯ = { toList := toList✝ }.set i b h

Proof state:
case mk
α : Type u_1
a b : α
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ ({ toList := toList✝ }.set i a h).set i b ⋯ = { toList := toList✝ }.set i b h

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasSum_coe {f : α → ℝ≥0} {r : ℝ≥0} :
    HasSum (fun a => (f a : ℝ≥0∞)) ↑r ↔ HasSum f r

Proof state:
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r

Tactic:
simp only [HasSum, ← coe_finset_sum, tendsto_coe]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_top : succ (⊤ : α) = ⊤

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : OrderTop α
⊢ succ ⊤ = ⊤

Tactic:
rw [succ_eq_iff_isMax, isMax_iff_eq_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Φ_three : W.Φ 3 = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ Even 2

Tactic:
decide

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 3 = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

Tactic:
rw [show 3 = ((2 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_three, if_pos <| by decide, mul_one,
  preΨ'_four, preΨ'_two, mul_one, if_pos even_two]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 3 = ↑2 + 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_map_complex (f : E ≃ₗᵢ[ℝ] ℂ)
    (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : E) :
    o.kahler x y = conj (f x) * f y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.kahler x) y = (o.kahler x) (f.symm (f y))

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.kahler x) y = (o.kahler (f.symm (f x))) (f.symm (f y))

Tactic:
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.kahler x) y = (starRingEnd ℂ) (f x) * f y

Tactic:
rw [← Complex.kahler, ← hf, kahler_map (hF := _)]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.kahler x) y = (o.kahler (f.symm (f x))) (f.symm (f y))