harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Map.lean
theorem Filter.map_surjOn_Iic_iff_le_map {m : α → β} :
    SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Proof state:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
H : Filter β
hHG : H ≤ G
⊢ map m ((fun x => F ⊓ comap m x) H) = H

Tactic:
simpa [Filter.push_pull] using hHG.trans hm

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : SurjOn (map m) (Iic F) (Iic G)
⊢ G ≤ map m F

Tactic:
rcases hm right_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩

Result:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
F : Filter α
m : α → β
H : Filter α
hHF : H ≤ F
hm : SurjOn (map m) (Iic F) (Iic (map m H))
⊢ map m H ≤ map m F

Proof state:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
F : Filter α
m : α → β
H : Filter α
hHF : H ≤ F
hm : SurjOn (map m) (Iic F) (Iic (map m H))
⊢ map m H ≤ map m F

Tactic:
exact map_mono hHF

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
this : RightInvOn (fun x => F ⊓ comap m x) (map m) (Iic G)
⊢ SurjOn (map m) (Iic F) (Iic G)

Tactic:
exact this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Tactic:
refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : SurjOn (map m) (Iic F) (Iic G)
⊢ G ≤ map m F

case refine_2
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
⊢ SurjOn (map m) (Iic F) (Iic G)
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem mono_of_mono_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Mono h]
    (w : f ≫ g = h) : Mono f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Mono h
w : f ≫ g = h
⊢ Mono f

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ Mono f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ Mono f

Tactic:
exact mono_of_mono f g

Result:
no goals
-- Mathlib/RingTheory/Norm/Defs.lean
theorem norm_algebraMap_of_basis [Fintype ι] (b : Basis ι R S) (x : R) :
    norm R (algebraMap R S x) = x ^ Fintype.card ι

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι

Tactic:
haveI := Classical.decEq ι

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ((toMatrix b b) ((lsmul R R S) x)).det = x ^ Fintype.card ι

Tactic:
convert @det_diagonal _ _ _ _ _ fun _ : ι => x

Result:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (toMatrix b b) ((lsmul R R S) x) = diagonal fun x_1 => x

case h.e'_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ x ^ Fintype.card ι = ∏ i : ι, x

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι

Tactic:
rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ((toMatrix b b) ((lsmul R R S) x)).det = x ^ Fintype.card ι

Proof state:
case h.e'_2.h.e'_6.a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
i j : ι
⊢ (toMatrix b b) ((lsmul R R S) x) i j = diagonal (fun x_1 => x) i j

Tactic:
rw [toMatrix_lsmul]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ x ^ Fintype.card ι = ∏ i : ι, x

Tactic:
rw [Finset.prod_const, Finset.card_univ]

Result:
no goals

Proof state:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (toMatrix b b) ((lsmul R R S) x) = diagonal fun x_1 => x

Tactic:
ext (i j)

Result:
case h.e'_2.h.e'_6.a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
i j : ι
⊢ (toMatrix b b) ((lsmul R R S) x) i j = diagonal (fun x_1 => x) i j
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem tendstoUniformlyOn_iff {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
    TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, dist (f x) (F n x) < ε

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist 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

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

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

Result:
case intro.intro
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

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

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

Result:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toArray_range (n : Nat) : (range n).toArray = Array.range n

Proof state:
case h
n : Nat
⊢ (range n).toArray.toList = (Array.range n).toList

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
⊢ (range n).toArray = Array.range n

Tactic:
apply ext'

Result:
case h
n : Nat
⊢ (range n).toArray.toList = (Array.range n).toList
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β}
    (hf : UniformContinuous f) : UniformContinuous (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖))

Tactic:
rw [uniformContinuous_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖)

Tactic:
exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma posFittingCompOf_le_posFittingComp (x : L) :
    posFittingCompOf R M x ≤ posFittingComp R L M

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
x : L
⊢ posFittingCompOf R M x ≤ posFittingComp R L M

Tactic:
rw [posFittingComp]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
x : L
⊢ posFittingCompOf R M x ≤ ⨆ x, posFittingCompOf R M x

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
x : L
⊢ posFittingCompOf R M x ≤ ⨆ x, posFittingCompOf R M x

Tactic:
exact le_iSup (posFittingCompOf R M) x

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma subsingleton_iff_ker_eq_top (S : Submonoid R) (g : M →ₗ[R] M')
    [IsLocalizedModule S g] :
    Subsingleton M' ↔ LinearMap.ker g = ⊤

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
H : ⊤ ≤ LinearMap.ker g
x : M'
⊢ x = 0

Tactic:
obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S g x

Result:
case intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
H : ⊤ ≤ LinearMap.ker g
x : M
s : ↥S
⊢ Function.uncurry (mk' g) (x, s) = 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ LinearMap.ker g = ⊤

Tactic:
rw [← top_le_iff]

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ⊤ ≤ LinearMap.ker g

Proof state:
case intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
H : ⊤ ≤ LinearMap.ker g
x : M
s : ↥S
⊢ Function.uncurry (mk' g) (x, s) = 0

Tactic:
simpa using @H x Submodule.mem_top

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ⊤ ≤ LinearMap.ker g

Tactic:
refine ⟨fun H m _ ↦ Subsingleton.elim _ _, fun H ↦ (subsingleton_iff_forall_eq 0).mpr fun x ↦ ?_⟩

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
H : ⊤ ≤ LinearMap.ker g
x : M'
⊢ x = 0
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
/-- The maximal atlas of a structure groupoid is stable under equivalence. -/
lemma StructureGroupoid.mem_maximalAtlas_of_eqOnSource {e e' : PartialHomeomorph M H} (h : e' ≈ e)
    (he : e ∈ G.maximalAtlas M) : e' ∈ G.maximalAtlas M

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : PartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
⊢ e' ∈ maximalAtlas M G

Tactic:
intro e'' he''

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : PartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
e'' : PartialHomeomorph M H
he'' : e'' ∈ atlas H M
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G

Proof state:
case intro
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : PartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
e'' : PartialHomeomorph M H
he'' : e'' ∈ atlas H M
l : e.symm ≫ₕ e'' ∈ G
r : e''.symm ≫ₕ e ∈ G
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G

Tactic:
exact ⟨G.mem_of_eqOnSource l (EqOnSource.trans' (EqOnSource.symm' h) (e''.eqOnSource_refl)),
       G.mem_of_eqOnSource r (EqOnSource.trans' (e''.symm).eqOnSource_refl h)⟩

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : PartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
e'' : PartialHomeomorph M H
he'' : e'' ∈ atlas H M
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G

Tactic:
obtain ⟨l, r⟩ := mem_maximalAtlas_iff.mp he e'' he''

Result:
case intro
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : PartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
e'' : PartialHomeomorph M H
he'' : e'' ∈ atlas H M
l : e.symm ≫ₕ e'' ∈ G
r : e''.symm ≫ₕ e ∈ G
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
@[simp]
lemma chainLength_neg :
    chainLength (-α) β = chainLength α β

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ chainLength (-α) β = chainLength α β

Tactic:
rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
  Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_neg]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_whiskerLeft {p : a ⟶ b} {f : b ⟶ c} {g h : c ⟶ d} {pf : a ⟶ c} {pfg : a ⟶ d}
    {η : g ≅ h} (η_f : p ≫ f ≅ pf) (η_fg : pf ≫ g ≅ pfg) (η_fh : pf ≫ h ≅ pfg)
    (ih_η : pf ◁ η ≪≫ η_fh = η_fg) :
    p ◁ (f ◁ η) ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Tactic:
rw [← ih_η]

Result:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom

Tactic:
simp [← whisker_exchange_assoc]

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)

Tactic:
apply Iso.ext (by simp [← whisker_exchange_assoc])

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem stronglyMeasurable (f : α →ₘ[μ] β) : StronglyMeasurable f

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (const α (Classical.choose h))

Tactic:
exact stronglyMeasurable_const

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ StronglyMeasurable ↑f

Tactic:
simp only [cast]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ StronglyMeasurable
    (if h : ∃ b, f = mk (const α b) ⋯ then const α (Classical.choose h)
    else AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ StronglyMeasurable
    (if h : ∃ b, f = mk (const α b) ⋯ then const α (Classical.choose h)
    else AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (const α (Classical.choose h))

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)

Tactic:
apply AEStronglyMeasurable.stronglyMeasurable_mk

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
theorem Finite.pi (ht : ∀ i, (t i).Finite) : (pi univ t).Finite

Proof state:
case intro.intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (↑(Fintype.piFinset t)).Finite

Tactic:
apply Finset.finite_toSet

Result:
no goals

Proof state:
case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
val✝ : Fintype ι
⊢ (univ.pi t).Finite

Tactic:
lift t to ∀ d, Finset (κ d) using ht

Result:
case intro.intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (univ.pi fun i => ↑(t i)).Finite

Proof state:
case intro.intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (univ.pi fun i => ↑(t i)).Finite

Tactic:
classical
  rw [← Fintype.coe_piFinset]
  apply Finset.finite_toSet

Result:
no goals

Proof state:
case intro.intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (univ.pi fun i => ↑(t i)).Finite

Tactic:
rw [← Fintype.coe_piFinset]

Result:
case intro.intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (↑(Fintype.piFinset t)).Finite

Proof state:
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ (univ.pi t).Finite

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
val✝ : Fintype ι
⊢ (univ.pi t).Finite
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem ext' {f₁ f₂ : M ≃ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
⊢ f₁ = f₂

Tactic:
ext x

Result:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x

Proof state:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)

Tactic:
simp only [map_sum, LinearEquiv.map_smulₛₗ, h]

Result:
no goals

Proof state:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x

Tactic:
rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]

Result:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem intCast (n : ℤ) : mapFun f (n : 𝕎 R) = n :=
  show mapFun f n.castDef = (n : WittVector p S) by
    cases n <;> simp [*, Int.castDef, add, one, neg, zero, natCast] <;> rfl

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n : ℤ
⊢ mapFun (⇑f) n.castDef = ↑n

Tactic:
cases n <;> simp [*, Int.castDef, add, one, neg, zero, natCast] <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem _root_.exists_prime_addOrderOf_dvd_card {G : Type*} [AddGroup G] [Fintype G] (p : ℕ)
    [Fact p.Prime] (hdvd : p ∣ Fintype.card G) : ∃ x : G, addOrderOf x = p :=
  @exists_prime_orderOf_dvd_card (Multiplicative G) _ _ _ _ (by convert hdvd)

Proof state:
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card (Multiplicative G)

Tactic:
convert hdvd

Result:
no goals