mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ b1 * a * (b * a2) = b1 * a1 * (b2 * a2)

pp: G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
a b : G
hu : b1 * a = b1 * a1 ∧ b * a2 = b2 * a2
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ a = a1 ∧ b = b2

Tactic:
· rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]

Goal state after:
G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
a b : G
hu : b1 * a = b1 * a1 ∧ b * a2 = b2 * a2
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ a = a1 ∧ b = b2
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
⊢ t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Goal state after:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑t
b : α
hb : b ∈ ↑t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)

Tactic:
cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_left, *]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
⊢ s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Goal state after:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = map (lsingle a) (span R s)

Tactic:
rw [← span_image]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = span R (⇑(lsingle a) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_1.single
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ (lmapDomain R R u) (single i s) ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
| single i s =>

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

Goal state before:
pp: case refine_1.zero
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (lmapDomain R R u) 0 ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ 0 ∈ span R {x | ∃ i x_1, single i x_1 = x}

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r ^ 0 = (monomial (n * 0)) (r ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
⊢ (monomial 0) 1 = X ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ X ^ 0 * p = p * X ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X ^ 0 = (monomial (n + 0)) r

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
a : R
⊢ motive (Polynomial.C a * X ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1
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
x✝ : Mul (Finset G) := Finset.mul
⊢ (image (fun x ↦ x⁻¹) D * C).Nonempty

Tactic:
apply_rules [Nonempty.mul, Nonempty.image, Finset.Nonempty.map, hc.1, hc.2.1]

Goal state after:
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
x✝ : Mul (Finset G) := Finset.mul
⊢ (D * image (fun x ↦ x⁻¹) C).Nonempty

Tactic:
apply_rules [Nonempty.mul, Nonempty.image, Finset.Nonempty.map, hc.1, hc.2.1]

Goal state after:
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:
mem_product,

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 a2 b2 : G
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
h1 : a1 ∈ image (⇑f) A ∧ b1 ∈ image (⇑f) B
h2 : a2 ∈ image (⇑f) A ∧ b2 ∈ image (⇑f) B
⊢ ∃ p1,
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ ∃ p2, (p2.1 ∈ A ∧ p2.2 ∈ 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:
mem_product,

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 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 : p1.1 ∈ image (fun x ↦ x i) A ∧ p1.2 ∈ image (fun x ↦ x i) B
h2 : p2.1 ∈ image (fun x ↦ x i) A ∧ p2.2 ∈ image (fun x ↦ x i) B
⊢ ∃ 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.Exact.Basic

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
⊢ (g' ∘ g) x = 1 ↔ x ∈ Set.range f

Tactic:
refine ⟨fun H => mulExact x |>.mp <| inj <| h0 ▸ H, ?_⟩

Goal state after:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
⊢ x ∈ Set.range f → (g' ∘ g) x = 1
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
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
⊢ ∀ (x y : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)), ofIsCompl h (x + y).1 (x + y).2 = ofIsCompl h x.1 x.2 + ofIsCompl h y.1 y.2

Tactic:
intro φ

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
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
⊢ ∀ (y : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)), ofIsCompl h (φ + y).1 (φ + y).2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h y.1 y.2
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
n : ℕ
⊢ (↑n).succ = ↑n + 1

Tactic:
rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]

Goal state after:
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 : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ Function.Injective ⇑(f.prod g)

Tactic:
simp [← ker_eq_bot, hfg.inf_eq_bot]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
S : SetRel β β
R : SetRel α β
inst✝ : S.IsRefl
⊢ R ⊆ R ○ S

Tactic:
simpa using comp_subset_comp_right id_subset

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

Goal state before:
pp: G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
⊢ UniqueMul A B a0 b0

Tactic:
intro a

Goal state after:
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a : G
⊢ ∀ ⦃b : G⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
⊢ UniqueMul A B (a1, b1).1 (a1, b1).2

Tactic:
intro a

Goal state after:
case refine_2
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a : G
⊢ ∀ ⦃b : G⦄, a ∈ A → b ∈ B → a * b = (a1, b1).1 * (a1, b1).2 → a = (a1, b1).1 ∧ b = (a1, b1).2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
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
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_3_to_1 : (∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e) → Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
⊢ Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id

Tactic:
have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
    exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.mem
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ x ∈ s, ∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
intro a

Goal state after:
case a.mem
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
⊢ a ∈ s → ∀ n ∈ span R t, (f a) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
heq : p.length = 0
⊢ motive p

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
⊢ motive p

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ x ∈ s, ∀ y ∈ t, (f x) y ∈ ↑(map₂ f (span R s) (span R t))

Tactic:
intro a

Goal state after:
case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
⊢ a ∈ s → ∀ y ∈ t, (f a) y ∈ ↑(map₂ f (span R s) (span R t))
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
M₂ : Type u_5
N₂ : Type u_6
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R M₂
inst✝ : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q

Tactic:
rw [map₂_map_right, map₂_map_left]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
M₂ : Type u_5
N₂ : Type u_6
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R M₂
inst✝ : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.compl₂ h ∘ₗ g) p q = map₂ (f.compl₁₂ g h) p q
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp.zero
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ ∃ x, x.length = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) → ∀ (n : ℕ), ∃ x, x.length = n

Tactic:
intro H n
    induction n with
    | zero => refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
    | succ n IH =>
      obtain ⟨l, hl⟩ := IH
      obtain ⟨l', hl'⟩ := H l
      exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : Fin (0 + 1) → α
h : ∀ (i : Fin 0), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
⊢ ∃ t i,
    t.toFun ∘ ⇑i = { length := 0, toFun := s, step := h }.toFun ∧
      i 0 = 0 ∧ i (Fin.last { length := 0, toFun := s, step := h }.length) = Fin.last t.length

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.zero
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 0
⊢ ↑0 ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos.zero
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
hn : n = 0
⊢ height a = ↑0 ↔ Minimal (fun y ↦ ↑0 ≤ height y) a

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
| m ⊗ₜ[R] (r • n)

Tactic:
← one_smul R n

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
| m ⊗ₜ[R] (r • 1 • n)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderBot,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]
  simp [Order.krullDim_nonneg]

Goal state after: