mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)

Tactic:
simp [Set.image_inter hf]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
⊢ IsSMulRegular R[X] s

Tactic:
by
    rintro ⟨f⟩ ⟨g⟩ hfg; congr; apply hs.isSMulRegular; simpa using congr(($hfg).toFinsupp)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (x y : R), (monomial 0).toFun (x * y) = (monomial 0).toFun x * (monomial 0).toFun y

Tactic:
simp [monomial_mul_monomial]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥

Tactic:
[

Goal state after:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
hu' :
  { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' =
      { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 →
    { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' = { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∧
      { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' = { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
[

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
hu' :
  { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' =
      { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 →
    { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' = { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∧
      { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' = { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
he : X = C a
⊢ False

Tactic:
simpa using monomial_eq_monomial_iff.1 he

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ ((lsum R) fun x ↦ f x • φ).range = Set.range f • φ.range

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ ((lsum R) fun x ↦ f x • φ).range = Set.range f • φ.range
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ coeff 1 n = if n = 0 then 1 else 0

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ coeff 1 n = if n = 0 then 1 else 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i ∈ p.support, q.sum fun j a ↦ (monomial (i + j)) (p.coeff i * a)).toFinsupp

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i ∈ p.support, q.sum fun j a ↦ (monomial (i + j)) (p.coeff i * a)).toFinsupp
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun n a ↦ C a * X ^ n) = p

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun n a ↦ C a * X ^ n) = p
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ single n (p.coeff n) + AddMonoidAlgebra.erase n p.toFinsupp = p.toFinsupp

Tactic:
exact AddMonoidAlgebra.single_add_erase ..

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ coeffs 1 ⊆ {1}
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ p ≤ Submodule.comap (↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e) p ↔ p ≤ Submodule.comap f p

Tactic:
this

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ p ≤ Submodule.comap f p ↔ p ≤ Submodule.comap f p
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  (linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) =
    (mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)
⊢ Function.Injective ⇑(linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd))

Tactic:
this

Goal state after:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  (linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) =
    (mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)
⊢ Function.Injective ⇑((mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R))
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n f, f.range = N

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n f, f.range = N
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inl
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < #(image (⇑f) A) * #(image (⇑f) B)
a1 b1 : G
h1 : (a1, b1) ∈ image (⇑f) A ×ˢ image (⇑f) B
a2 b2 : G
h2 : (a2, b2) ∈ image (⇑f) A ×ˢ image (⇑f) B
hne : (a1, b1) ≠ (a2, b2)
hu1 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a1, b1).1 (a1, b1).2
hu2 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a2, b2).1 (a2, b2).2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
[

Goal state after:
case inl
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < #(image (⇑f) A) * #(image (⇑f) B)
a1 b1 : G
h1 : (a1, b1) ∈ image (⇑f) A ×ˢ image (⇑f) B
a2 b2 : G
h2 : (a2, b2) ∈ image (⇑f) A ×ˢ image (⇑f) B
hne : (a1, b1) ≠ (a2, b2)
hu1 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a1, b1).1 (a1, b1).2
hu2 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a2, b2).1 (a2, b2).2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: 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 : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
p1 : G i × G i
h1 : p1 ∈ image (fun x ↦ x i) A ×ˢ image (fun x ↦ x i) B
p2 : G i × G i
h2 : p2 ∈ image (fun x ↦ x i) A ×ˢ image (fun x ↦ x i) B
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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
[

Goal state after:
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 : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
p1 : G i × G i
h1 : p1 ∈ image (fun x ↦ x i) A ×ˢ image (fun x ↦ x i) B
p2 : G i × G i
h2 : p2 ∈ image (fun x ↦ x i) A ×ˢ image (fun x ↦ x i) B
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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ x - (p.projection q h) x ∈ q

Tactic:
rw [← projection_eq_self_sub_projection h]
  exact projection_apply_mem h.symm x

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2.refine_2
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 : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
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
a1 : (i : ι) → G i
ha1 : a1 ∈ A ∧ a1 i = p1.1
b1 : (i : ι) → G i
hb1 : b1 ∈ B ∧ b1 i = p1.2
hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1
a2 : (i : ι) → G i
ha2 : a2 ∈ A ∧ a2 i = p2.1
b2 : (i : ι) → G i
hb2 : b2 ∈ B ∧ b2 i = p2.2
hu2 : UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a2 b2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
[

Goal state after:
case refine_2.refine_2
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 : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
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
a1 : (i : ι) → G i
ha1 : a1 ∈ A ∧ a1 i = p1.1
b1 : (i : ι) → G i
hb1 : b1 ∈ B ∧ b1 i = p1.2
hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1
a2 : (i : ι) → G i
ha2 : a2 ∈ A ∧ a2 i = p2.1
b2 : (i : ι) → G i
hb2 : b2 ∈ B ∧ b2 i = p2.2
hu2 : UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a2 b2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ ofIsCompl ⋯ ψ φ = ofIsCompl hpq φ ψ

Tactic:
simp [ofIsCompl_eq_add, add_comm]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case top
s : Set ℕ∞
h : s.Infinite
hx : ⊤ < ⊤
⊢ ∃ a ∈ s, ⊤ < a

Tactic:
simp at hx

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ (⨆ i, f i) * a = ⨆ i, f i * a

Tactic:
[

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ (⨆ i, f i) * a = ⨆ i, f i * a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
⊢ a * sSup s = ⨆ b ∈ s, a * b

Tactic:
[

Goal state after:
s : Set ℕ∞
a : ℕ∞
⊢ a * sSup s = ⨆ b ∈ s, a * b
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
⊢ sSup s * a = ⨆ b ∈ s, b * a

Tactic:
[

Goal state after:
s : Set ℕ∞
a : ℕ∞
⊢ sSup s * a = ⨆ b ∈ s, b * a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
[

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
[

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x : E
⊢ ↑f x ∈ p

Tactic:
[

Goal state after:
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x : E
⊢ ↑f x ∈ p
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
[

Goal state after:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
[

Goal state after:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Exact ⇑f ⇑g

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Exact ⇑f ⇑g
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
[

Goal state after:
R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
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 inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g

Tactic:
[

Goal state after:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g

Tactic:
[

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
[

Goal state after:
ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range

Tactic:
[

Goal state after:
S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T

Tactic:
[

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
h : Commute f T
⊢ f * (T * f) = T * f ∧ f * (T * f) = f * T

Tactic:
by simp [← h.eq, ← mul_assoc, hf.eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑T ↔ map (↑T) f.range = f.range ∧ map (↑T) f.ker = f.ker

Tactic:
[

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑T ↔ map (↑T) f.range = f.range ∧ map (↑T) f.ker = f.ker
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x.toList

Tactic:
[

Goal state after:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x.toList
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B✝) * #(map f A✝)
p1 : Gᵐᵒᵖ × Gᵐᵒᵖ
h1 : p1 ∈ map f B✝ ×ˢ map f A✝
p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
h2 : p2 ∈ map f B✝ ×ˢ map f A✝
hne : p1 ≠ p2
hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2
hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2
⊢ ∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2

Tactic:
[

Goal state after:
G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B✝) * #(map f A✝)
p1 : Gᵐᵒᵖ × Gᵐᵒᵖ
h1 : p1 ∈ map f B✝ ×ˢ map f A✝
p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
h2 : p2 ∈ map f B✝ ×ˢ map f A✝
hne : p1 ≠ p2
hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2
hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2
⊢ ∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2