mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ factorThruImageSubobject f ≫ (imageSubobject f).arrow = f

Tactic:
by
  simp [factorThruImageSubobject]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
S : ShortComplex C := { X₁ := Limits.kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ }
hS : (S.map F).Exact ∧ Mono (F.map S.f) := hF S ⟨exact_kernel f, inferInstance⟩
⊢ IsLimit (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) F)

Tactic:
have : Mono (S.map F).f := hS.2

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
S : ShortComplex C := { X₁ := Limits.kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ }
hS : (S.map F).Exact ∧ Mono (F.map S.f) := hF S ⟨exact_kernel f, inferInstance⟩
this : Mono (S.map F).f
⊢ IsLimit (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) F)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ x✝ : Subobject A
⊢ ThinSkeleton.mk (representative.obj f₁) ⊓ x✝ = (inf.obj (Quotient.mk'' (representative.obj f₁))).obj x✝

Tactic:
congr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
⊢ (opProductIsoCoproduct Z).inv ≫ (Pi.lift π).op = Sigma.desc fun a ↦ (π a).op

Tactic:
convert!
    opProductIsoCoproduct'_inv_comp_lift (productIsProduct Z) (coproductIsCoproduct (op <| Z ·))
      (Fan.mk _ π)

Goal state after:
case e'_2.e'_7.e'_5
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
e_4✝¹ : op (∏ᶜ Z) = op (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
e_5✝ : op X = op (Fan.mk X π).pt
e_3✝ : X = (Fan.mk X π).pt
e_4✝ : ∏ᶜ Z = (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
⊢ Pi.lift π = (productIsProduct Z).lift (Fan.mk X π)

case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
⊢ (Sigma.desc fun a ↦ (π a).op) = (coproductIsCoproduct fun x ↦ op (Z x)).desc (Fan.mk X π).op
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ f.app i ≫ colimit.ι Y✝ i ≫ ((L.lan.obj Y✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app Y✝)).inv =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).inv ≫ colimMap (L.lan.map f)

Tactic:
ι_colimitIsoOfIsLeftKanExtension_inv,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ f.app i ≫ (L.lanUnit.app Y✝).app i ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).inv ≫ colimMap (L.lan.map f)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
Y : D
j : CostructuredArrow L Y
⊢ colimit.ι (CostructuredArrow.proj L Y ⋙ F) ((CostructuredArrow.map (𝟙 Y)).obj j) =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j

Tactic:
congr

Goal state after:
case e_7
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
Y : D
j : CostructuredArrow L Y
⊢ (CostructuredArrow.map (𝟙 Y)).obj j = j
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
⊢ limit.π (StructuredArrow.proj Y L ⋙ F) ((StructuredArrow.map (𝟙 Y)).obj j) = limit.π (StructuredArrow.proj Y L ⋙ F) j

Tactic:
congr

Goal state after:
case e_7
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
⊢ (StructuredArrow.map (𝟙 Y)).obj j = j
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ limit.π (StructuredArrow.proj X L ⋙ F) j =
    limit.π (StructuredArrow.proj X L ⋙ F) (StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right)))

Tactic:
congr

Goal state after:
case e_7
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesLimit K colim

Tactic:
refine preservesLimit_of_natIso K (?_ : e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop

Tactic:
congr

Goal state after:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| f.unop.left

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| (Subobject.underlyingIso f.unop.left.op).hom.unop
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop

Tactic:
congr

Goal state after:
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| g.unop.left

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
x : (Discrete.functor F).ColimitType
⊢ ∀ ⦃a₂ : (Discrete.functor F).ColimitType⦄,
    (Discrete.functor F).descColimitType c x = (Discrete.functor F).descColimitType c a₂ → x = a₂

Tactic:
y

Goal state after:
case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
x y : (Discrete.functor F).ColimitType
⊢ (Discrete.functor F).descColimitType c x = (Discrete.functor F).descColimitType c y → x = y
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ Additive.toMul (↑z • Additive.ofMul u) = u ^ z

Tactic:
rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 : ∀ (m : M), f m = ↑a ⟨i m, ⋯⟩
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄ ⦃hb : x ∈ b.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = b

Tactic:
congr

Goal state after:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 : ∀ (m : M), f m = ↑a ⟨i m, ⋯⟩
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄ ⦃hb : x ∈ b.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ a = b.toLinearPMap
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
x : N
y : x ∈ (X ⊓ Y).domain
h : x ∈ (X.toLinearPMap ⊓ Y.toLinearPMap).domain
⊢ ↑(X ⊓ Y).toLinearPMap ⟨x, y⟩ = ↑(X.toLinearPMap ⊓ Y.toLinearPMap) ⟨x, h⟩

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
y : N
z1 z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 + z2) • y, ⋯⟩ =
    ↑(extensionOfMax i f).toLinearPMap (⟨↑z1 • y, ⋯⟩ + ⟨↑z2 • y, ⋯⟩)

Tactic:
congr

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
y : N
z1 z2 : ↥(ideal i f y)
⊢ ↑(z1 + z2) • y = ↑⟨↑z1 • y, ⋯⟩ + ↑⟨↑z2 • y, ⋯⟩
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap ⟨a + (r • y - snd i x • y), ⋯⟩ + (extendIdealTo i f h y) (snd i x)

Tactic:
congr

Goal state after:
case e_a
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ fst i x = ⟨a + (r • y - snd i x • y), ⋯⟩
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ r •
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a)) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
congr

Goal state after:
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun x ↦ p x) ∘ fun x ↦ x % a) (Ico n (n + a)))

Tactic:
congr

Goal state after:
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = (fun x ↦ p x) ∘ fun x ↦ x % a
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap (⟨x, ⋯⟩ + ⟨y, ⋯⟩)

Tactic:
congr

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ x.Coprime q

Tactic:
rwa [gcd_mul_left, mul_eq_left hd0.ne'] at hb2

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)

Tactic:
rw [← sub_right_comm, Set.sub_mem_Ico_iff_left, add_right_comm]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)
Module: Mathlib.Topology.ContinuousMap.Defs

Goal state before:
pp: case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toFun✝¹ : X → Y
continuous_toFun✝¹ : Continuous[inst✝¹, inst✝] toFun✝¹
toFun✝ : X → Y
continuous_toFun✝ : Continuous[inst✝¹, inst✝] toFun✝
h :
  { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen[inst✝] (f i ∩ s)
⊢ IsOpen[inst✝] (univ ∩ s)

Tactic:
← hU,

Goal state after:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen[inst✝] (f i ∩ s)
⊢ IsOpen[inst✝] ((⋃ i, f i) ∩ s)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ (𝓟 ∘ g) univ = ⊤

Tactic:
Function.comp_apply,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ 𝓟 (g univ) = ⊤
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ ((g₁ x).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) =
    f₂.lift fun t ↦ (g₁ x).lift fun s ↦ (g₂ t).lift' fun t ↦ s ×ˢ t

Tactic:
lift_comm

Goal state after:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ ((g₁ x).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) =
    (g₁ x).lift fun t ↦ f₂.lift fun s ↦ (g₂ s).lift' fun t_1 ↦ t ×ˢ t_1
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ ((g₁ x).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) =
    f₂.lift fun t ↦ (g₁ x).lift fun s ↦ (g₂ t).lift' fun t ↦ s ×ˢ t

Tactic:
rw [lift_comm]

Goal state after:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ ((g₁ x).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) =
    (g₁ x).lift fun t ↦ f₂.lift fun s ↦ (g₂ s).lift' fun t_1 ↦ t ×ˢ t_1
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ ⋃ s ∈ range f, closure s = ⋃ i, closure (f i)

Tactic:
biUnion_range

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ ⋃ y, closure (f y) = ⋃ i, closure (f i)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ closure (⋃ i, f i) = ⋃ i, closure (f i)

Tactic:
rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ (interior s)ᶜ = univ

Tactic:
compl_univ_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ interior s = ∅
Module: Mathlib.Topology.Defs.Induced

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
h : ∀ t_1 ∈ S, ∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = t_1
⊢ ∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S

Tactic:
choose! g hgo hfg using h
    refine ⟨⋃₀ (g '' S), isOpen_sUnion <| forall_mem_image.2 hgo, ?_⟩
    rw [preimage_sUnion, biUnion_image, sUnion_eq_biUnion]
    exact iUnion₂_congr hfg

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t

Tactic:
rintro ⟨⟨u, u_cov, u_props⟩, ⟨v, v_cov, v_props⟩⟩

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
⊢ SeparatedNhds s t
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {u : Set X}, IsOpen[inst✝¹] u → IsOpen[inst✝] (kernImage f u)

Tactic:
rw [IsClosedMap, compl_surjective.forall]
  simp [kernImage_eq_compl]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ∀ (b : X), Disjoint (𝓝 x) (𝓝 b) → {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, b)

Tactic:
y

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x y : X
⊢ Disjoint (𝓝 x) (𝓝 y) → {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x

Tactic:
by
  rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ DenseRange (inclusion hst) ↔ t ⊆ closure[inst✝] s

Tactic:
by
  rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]

Goal state after: