mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = finrank ℝ ↥(vectorSpan ℝ (Set.range t₁.points))

Tactic:
t₁.independent.finrank_vectorSpan (Fintype.card_fin _),

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = 2
Module: Mathlib.Geometry.Manifold.DerivationBundle

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ v (ContMDiffMap.comp (k • g) f) = k * v (ContMDiffMap.comp g f)

Tactic:
ContMDiffMap.smul_comp,

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ v (k • ContMDiffMap.comp g f) = k * v (ContMDiffMap.comp g f)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ Disjoint (ModelWithCorners.interior M) (ModelWithCorners.boundary M)

Tactic:
by_contra h

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : ¬Disjoint (ModelWithCorners.interior M) (ModelWithCorners.boundary M)
⊢ False
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
t : Triangle ℝ P
ht : Set.range t.points ⊆ s
t₀ : Triangle ℝ P
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
⊢ s = insert t.orthocenter (Set.range t.points)

Tactic:
rw [ht₀s] at ht

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
⊢ s = insert t.orthocenter (Set.range t.points)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑I (extend Sum.inl (↑(chartAt H x)) (fun x_1 ↦ Classical.arbitrary H) (Sum.inl x)) ∈
    interior (I.target ∩ ↑I.symm ⁻¹' (chartAt H x).target)

Tactic:
Sum.inl_injective.extend_apply (chartAt H x)

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑I (↑(chartAt H x) x) ∈ interior (I.target ∩ ↑I.symm ⁻¹' (chartAt H x).target)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ ↑I (extend Sum.inl (↑(chartAt H x)) (fun x_1 ↦ Classical.arbitrary H) (Sum.inl x)) ∈ frontier (range ↑I)

Tactic:
Sum.inl_injective.extend_apply (chartAt H x)

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ ↑I (↑(chartAt H x) x) ∈ frontier (range ↑I)
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (interior (range Subtype.val)).Nonempty

Tactic:
rw [range_euclideanHalfSpace, interior_halfSpace]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ {y | 0 < y.ofLp 0}.Nonempty
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ 0 < ↑p - x

Tactic:
norm_num [hp.1]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
E' : Type u_6
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this✝ : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x := ⋯
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x := ⋯
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
F : E → E' := ⋯
hF : F = (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hFx₀ : ↑(extChartAt I' (f x₀)) (f x₀) = F (↑(extChartAt I x₀) x₀)
Y : (x : M') → TangentSpace I' x
this : (extChartAt I x₀).target ∈ 𝓝[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀) x₀
y : E
hy : y ∈ ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
h'''y : y ∈ (extChartAt I x₀).target
h'y : f (↑(extChartAt I x₀).symm y) ∈ (extChartAt I' (f x₀)).source
h''y : f (↑(extChartAt I x₀).symm y) ∈ (chartAt H' (f x₀)).source
⊢ y ∈ (extChartAt I x₀).target ∩ ↑(extChartAt I x₀).symm ⁻¹' s

Tactic:
exact ⟨h'''y, hy.1⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
⊢ (mfderiv% Subtype.val z) 1 = 1

Tactic:
have A : mfderiv[Icc x y] (Subtype.val ∘ (projIcc x y h.out.le)) z 1
      = mfderiv[Icc x y] (@id ℝ) z 1 := by
    congr 1
    apply mfderivWithin_congr_of_mem _ z.2
    intro z hz
    simp [projIcc_of_mem h.out.le hz]
  rw [← mfderivWithin_comp_projIcc_one, A]
  simp only [id_eq, mfderivWithin_eq_fderivWithin]
  rw [fderivWithin_id (uniqueDiffOn_Icc h.out _ z.2)]
  rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case refine_1.st
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := ⋯
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ univ ⊆ η ⁻¹' Icc 0 1

Tactic:
intro t ht
      exact ⟨Real.smoothTransition.nonneg _, Real.smoothTransition.le_one _⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁶ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝²⁵ : NormedAddCommGroup EM
inst✝²⁴ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝²³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace 𝕜 E
H : Type u_5
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst✝¹⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁶ : TopologicalSpace N
inst✝¹⁵ : ChartedSpace H N
inst✝¹⁴ : TopologicalSpace G
inst✝¹³ : ChartedSpace H G
inst✝¹² : TopologicalSpace A
inst✝¹¹ : ChartedSpace H A
inst✝¹⁰ : TopologicalSpace A'
inst✝⁹ : ChartedSpace H' A'
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ChartedSpace H R
EP : Type u_7
inst✝⁶ : NormedAddCommGroup EP
inst✝⁵ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁴ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝³ : TopologicalSpace P
inst✝² : ChartedSpace HP P
inst✝¹ : Ring R
inst✝ : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M)) (smoothPresheafRing IM I M R)

Tactic:
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget RingCat)]
    exact (smoothSheaf IM I M R).property

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
⊢ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) = ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
by
  ext1 f
  rw [mem_nonunits_iff, not_iff_comm, Iff.comm]
  apply smoothSheafCommRing.isUnit_stalk_iff

Goal state after:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E'') n (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm)
    (h.domChart.extend I).target

Tactic:
have : CMDiff n (Prod.fst ∘ h.equiv) := by rw [contMDiff_iff_contDiff]; fun_prop

Goal state after:
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
this : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E'') n (Prod.fst ∘ ⇑h.equiv)
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E'') n (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm)
    (h.domChart.extend I).target
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersion I J n f
x : M
⊢ IsSubmersionAt I J n f x

Tactic:
rw [IsSubmersionAt]
  use h.complement, by infer_instance, by infer_instance
  exact h.isSubmersionOfComplement_complement x

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
rcases fintypeOrInfinite G; swap
  · rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
  simp only [Nat.card_eq_fintype_card]
  calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
              (fun g ↦ card (MulAction.fixedBy G g))
              fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.eq
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
⊢ r 0 ≠ sr 0

Tactic:
by_contra h

Goal state after:
n : ℕ
h : r 0 = sr 0
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
⊢ Monoid.exponent (DihedralGroup 0) = lcm 0 2

pp: case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2

Tactic:
· exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one

Goal state after:
case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M ∗ N →* P
⊢ MonoidHom.mrange f = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)

Tactic:
rw [MonoidHom.mrange_eq_map, ← mrange_inl_sup_mrange_inr, Submonoid.map_sup, MonoidHom.map_mrange,
    MonoidHom.map_mrange]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
i : ι
x : G i
⊢ (lift f) (of x) ∈ s

Tactic:
simp only [lift_of]

Goal state after:
case of
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
i : ι
x : G i
⊢ (f i) x ∈ s
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ (lift f) (of x) = (f i) x

Tactic:
simp only [lift_of]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : m' = 1
⊢ False

Tactic:
simp only [rcons, dif_pos hm', dif_neg hm] at he

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
hm : ¬m = 1
hm' : m' = 1
he : cons m w ⋯ ⋯ = w'
⊢ False
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)

Tactic:
by
  have h₁ : ℓ (π (ω.take j)) ≤ (ω.take j).length := cs.length_wordProd_le (ω.take j)
  have h₂ : ℓ (π (ω.drop j)) ≤ (ω.drop j).length := cs.length_wordProd_le (ω.drop j)
  have h₃ := calc
    (ω.take j).length + (ω.drop j).length
    _ = ω.length := by rw [← List.length_append, ω.take_append_drop j]
    _ = ℓ (π ω) := hω.symm
    _ = ℓ (π (ω.take j) * π (ω.drop j)) := by rw [← cs.wordProd_append, ω.take_append_drop j]
    _ ≤ ℓ (π (ω.take j)) + ℓ (π (ω.drop j)) := cs.length_mul_le _ _
  unfold IsReduced
  lia

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a : α
s t : Set α
⊢ Set.image2 (fun x1 x2 ↦ x1 * x2) ((fun x ↦ x * a) '' s) t = Set.image2 (fun x1 x2 ↦ x1 * a * x2) s t

Tactic:
Set.image2_image_left

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ (fun x1 x2 ↦ x1 * x2) u r * s ∈ ↑(closure U) * R

Tactic:
show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ u * (r * s * (↑(f (r * s)))⁻¹) * ↑(f (r * s)) ∈ ↑(closure U) * R
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * (↑⟨r, hr⟩ * s⁻¹)⁻¹ ∈ ↑H

Tactic:
exact hR.toRightFun_mul_inv_mem (r * s⁻¹)

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 ↦ x1 * x2) g r ∈ H
⊢ r ∈ ↑H

Tactic:
exact (H.mul_mem_cancel_left (hU hg)).mp hh

Goal state after:
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
⊢ Odd (Nat.card G)

Tactic:
by_contra h

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : ¬Odd (Nat.card G)
⊢ False
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_2
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced ((replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
rw [replicate_succ', flatten_concat]
      refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h
      rw [← flatten_concat, ← replicate_succ']
      exact (h₁.flatten_replicate _).isReduced

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ ⊤.lowerCentralSeries n = ⊥ → nilpotencyClass G ≤ n

pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → ⊤.lowerCentralSeries n = ⊥

Tactic:
· intro h
    rw [← lowerCentralSeries_length_eq_nilpotencyClass]
    exact Nat.find_le h

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ¬⇑C.inclusion '' (g₁ • B) = ⇑C.inclusion '' (g₂ • B) →
      Disjoint (⇑C.inclusion '' (g₁ • B)) (⇑C.inclusion '' (g₂ • B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
Set.image_eq_image C.inclusion_injective,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ¬g₁ • B = g₂ • B → Disjoint (⇑C.inclusion '' (g₁ • B)) (⇑C.inclusion '' (g₂ • B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
⊢ B = Set.univ

Tactic:
rcases Set.eq_empty_or_nonempty B with rfl | hB_ne
  · simp at hB'
  have key := hB.ncard_block_mul_ncard_orbit_eq hB_ne
  rw [← key, mul_lt_mul_iff_of_pos_left (by rwa [Set.ncard_pos])] at hB'
  interval_cases (orbit G B).ncard
  · rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key
    exact (IsEmpty.exists_iff.mp hB_ne).elim
  · rw [mul_one, ← Set.ncard_univ] at key
    rw [Set.eq_of_subset_of_ncard_le (Set.subset_univ B) key.ge]

Goal state after: