mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
·

Goal state after:
case inl
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case hr
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
x : ↥f.ker
⊢ ((f ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯)) ∘ₗ inr R ↥p ↥f.ker) x =
    ((↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ id.prodMap 0) ∘ₗ inr R ↥p ↥f.ker) x

Tactic:
·

Goal state after:
case hr
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
x : ↥f.ker
⊢ ((f ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯)) ∘ₗ inr R ↥p ↥f.ker) x =
    ((↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ id.prodMap 0) ∘ₗ inr R ↥p ↥f.ker) x
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
⊢ Bijective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

pp: case refine_2
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
⊢ f = ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ?refine_1).symm.symm ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ?refine_1).symm

pp: case refine_3
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ g ∘ₗ ↑(↑e).symm ∘ₗ inr R M P = LinearMap.id

pp: case refine_4
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
⊢ LeftInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

pp: case refine_5
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
⊢ RightInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
⊢ Bijective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1.left
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Injective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

pp: case refine_1.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
·

Goal state after:
case refine_1.left
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Injective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊤ f
⊢ f = id

pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m id
⊢ m = ⊤

Tactic:
·

Goal state after:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊤ f
⊢ f = id
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m id
⊢ m = ⊤

Tactic:
·

Goal state after:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m id
⊢ m = ⊤
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊥ f
⊢ f = 0

pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ m = ⊥

Tactic:
·

Goal state after:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊥ f
⊢ f = 0
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ m = ⊥

Tactic:
·

Goal state after:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ m = ⊥
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
·

Goal state after:
case refine_1.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)
Module: Mathlib.Data.Rel

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = ∅

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = ∅
Module: Mathlib.Data.Rel

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA✝ : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA : ¬{a ∈ A | a i = p2.1} = A
⊢ 1 < #({a ∈ A | a i = p2.1}) * #({a ∈ B | a i = p2.2}) →
    ∃ p1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
      ∃ p2_1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
        p1 ≠ p2_1 ∧
          UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p1.1 p1.2 ∧
            UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p2_1.1 p2_1.2

Tactic:
·

Goal state after:
case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA✝ : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA : ¬{a ∈ A | a i = p2.1} = A
⊢ 1 < #({a ∈ A | a i = p2.1}) * #({a ∈ B | a i = p2.2}) →
    ∃ p1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
      ∃ p2_1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
        p1 ≠ p2_1 ∧
          UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p1.1 p1.2 ∧
            UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p2_1.1 p2_1.2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
⊢ f = ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm.symm ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm

pp: case refine_3
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ g ∘ₗ ↑(↑e).symm ∘ₗ inr R M P = LinearMap.id

pp: case refine_4
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
⊢ LeftInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

pp: case refine_5
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
⊢ RightInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
⊢ f = ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm.symm ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2.left
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ f = ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm.symm ∘ₗ inl R M P

pp: case refine_2.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm

Tactic:
·

Goal state after:
case refine_2.left
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ f = ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm.symm ∘ₗ inl R M P
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1.inr
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
⊢ 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2

Tactic:
·

Goal state after:
case refine_1.inr
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
⊢ 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm

Tactic:
·

Goal state after:
case refine_2.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ g ∘ₗ ↑(↑e).symm ∘ₗ inr R M P = LinearMap.id

pp: case refine_4
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
⊢ LeftInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

pp: case refine_5
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
⊢ RightInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ g ∘ₗ ↑(↑e).symm ∘ₗ inr R M P = LinearMap.id
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ 0 < s.length

Tactic:
by lia

Goal state after: