mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
    map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n)

Tactic:
ext

Goal state after:
n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ (map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))[i✝]? = some a✝ ↔
    (map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n))[i✝]? = some a✝
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
⊢ f = f' ∘ ⇑R

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
x✝ : ι
⊢ f x✝ = (f' ∘ ⇑R) x✝
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝² : Semiring α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
⊢ ⊥.primeCompl = nonZeroDivisors α

Tactic:
ext

Goal state after:
α : Type u
inst✝² : Semiring α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
x✝ : α
⊢ x✝ ∈ ⊥.primeCompl ↔ x✝ ∈ nonZeroDivisors α
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ aᶜᶜ = a

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ ↑aᶜᶜ = ↑a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ 0ᶜ = 1

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑0ᶜ = ↑1
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ 1ᶜ = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑1ᶜ = ↑0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a ∧ b * b = b

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a

case right
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ b * b = b
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) ↔ ∃ a, ∃ b ∈ I, a * y + b = x

Tactic:
constructor

Goal state after:
case mp
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) → ∃ a, ∃ b ∈ I, a * y + b = x

case mpr
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ a, ∃ b ∈ I, a * y + b = x) → ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y x✝ : α
⊢ x✝ * y = x ↔ x = y * x✝

Tactic:
by rw [eq_comm, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x : α
⊢ span {-x} = span {x}

Tactic:
ext

Goal state after:
α : Type u
inst✝ : Ring α
x x✝ : α
⊢ x✝ ∈ span {-x} ↔ x✝ ∈ span {x}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x + y, y} = span {x, y}

Tactic:
ext

Goal state after:
α : Type u
inst✝ : Ring α
x y x✝ : α
⊢ x✝ ∈ span {x + y, y} ↔ x✝ ∈ span {x, y}
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m i : ℕ
hi : i ∈ range (m + 1)
⊢ i ≤ 2 * m + 1

Tactic:
linarith [mem_range.1 hi]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x + y, y} = span {x, y}

Tactic:
by
  ext
  simp_rw [mem_span_pair]
  exact ⟨fun ⟨a, b, h⟩ => ⟨a, b + a, by rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]⟩,
    fun ⟨a, b, h⟩ => ⟨a, b - a, by rw [mul_add, sub_mul, add_add_sub_cancel, h]⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
x : α
inst✝ : LinearOrder α
⊢ span {|x|} = span {x}

Tactic:
obtain h | h := abs_choice x <;>
  simp [h]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x + y * z, y} = span {x, y}

Tactic:
ext

Goal state after:
α : Type u
inst✝ : CommRing α
x y z x✝ : α
⊢ x✝ ∈ span {x + y * z, y} ↔ x✝ ∈ span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x + y * z, y} = span {x, y}

Tactic:
by
  ext
  simp_rw [mem_span_pair]
  exact ⟨fun ⟨a, b, h⟩ => ⟨a, b + a * z, by rw [← h]; ring1⟩,
    fun ⟨a, b, h⟩ => ⟨a, b - a * z, by rw [← h]; ring1⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r : (i : ι) → R i
⊢ (pi fun x ↦ span {r x}) = span {r}

Tactic:
ext

Goal state after:
ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (x✝ ∈ pi fun x ↦ span {r x}) ↔ x✝ ∈ span {r}
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ Irreducible a

Tactic:
constructor

Goal state after:
case not_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ¬IsUnit a

case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ∀ ⦃a_1 b : α⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case a
n : ℕ
h : ¬n = 0
x✝ : ℕ
h' : x✝ ∈ range (n + 1)
⊢ (n - x✝) * n.choose (n - x✝) = (n - x✝) * n.choose x✝

Tactic:
choose_symm (mem_range_succ_iff.mp h')

Goal state after:
case a
n : ℕ
h : ¬n = 0
x✝ : ℕ
h' : x✝ ∈ range (n + 1)
⊢ (n - x✝) * n.choose x✝ = (n - x✝) * n.choose x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
⊢ factor ⋯ = RingHom.id (R ⧸ S)

Tactic:
ext

Goal state after:
R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
x✝ : R
⊢ ((factor ⋯).comp (mk S)) x✝ = ((RingHom.id (R ⧸ S)).comp (mk S)) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
⊢ (factor H2).comp (factor H1) = factor ⋯

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x✝ : R
⊢ (((factor H2).comp (factor H1)).comp (mk S)) x✝ = ((factor ⋯).comp (mk S)) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ (quotEquivOfEq h).symm = quotEquivOfEq ⋯

Tactic:
ext

Goal state after:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
x✝ : R ⧸ J
⊢ (quotEquivOfEq h).symm x✝ = (quotEquivOfEq ⋯) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
constructor

Goal state after:
case left
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I

case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ I.IsMaximal

Tactic:
by
  apply Ideal.isMaximal_iff.2
  constructor
  · intro h
    rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩
    exact hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))
  · intro J x hIJ hxnI hxJ
    rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩
    rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]
    exact J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite ↥?m.9 ∧ Finite (R ⧸ ?m.9)

Tactic:
constructor

Goal state after:
case left
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite ↥?m.9

case right
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite (R ⧸ ?m.9)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_5
inst✝ : Unique α
m : M
⊢ (finsuppUnique R M α).symm m = single default m

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_5
inst✝ : Unique α
m : M
⊢ ((finsuppUnique R M α).symm m) default = (single default m) default
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x y : α →₀ M
⊢ ⇑(x + y) = ⇑x + ⇑y

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x y : α →₀ M
x✝ : α
⊢ (x + y) x✝ = (⇑x + ⇑y) x✝
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x : R
y : α →₀ M
⊢ ⇑(x • y) = (RingHom.id R) x • ⇑y

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x : R
y : α →₀ M
x✝ : α
⊢ (x • y) x✝ = ((RingHom.id R) x • ⇑y) x✝
Module: Mathlib.LinearAlgebra.Finsupp.Pi

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
inst✝ : DecidableEq α
x : α
⊢ lcoeFun ∘ₗ lsingle x = LinearMap.single R (fun x ↦ M) x

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
x : α
x✝¹ : M
x✝ : α
⊢ (lcoeFun ∘ₗ lsingle x) x✝¹ x✝ = (LinearMap.single R (fun x ↦ M) x) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
⊢ (submodule fun x ↦ ⊤) = ⊤

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
x✝ : α →₀ M
⊢ (x✝ ∈ submodule fun x ↦ ⊤) ↔ x✝ ∈ ⊤
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u

Tactic:
constructor

Goal state after:
case mp
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) → ∃ u ∈ f, P u ∧ Q u

case mpr
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ x ∈ (mapRange.linearMap f).range ↔ x ∈ submodule fun x ↦ f.range

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ x ∈ (mapRange.linearMap f).range → x ∈ submodule fun x ↦ f.range

case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ (x ∈ submodule fun x ↦ f.range) → x ∈ (mapRange.linearMap f).range
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
⊢ (mapRange.linearMap f) { support := x.support, toFun := y, mem_support_toFun := ⋯ } = x

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
a✝ : I
⊢ ((mapRange.linearMap f) { support := x.support, toFun := y, mem_support_toFun := ⋯ }) a✝ = x a✝
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∈ x.support ↔ y i ≠ 0

Tactic:
constructor

Goal state after:
case mpr.mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∈ x.support → y i ≠ 0

case mpr.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ y i ≠ 0 → i ∈ x.support
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'

Tactic:
by
  simp only [hl'.ge_iff, hl.mem_iff]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊓ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊓ l' → ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

case mpr
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁

Tactic:
exact h.elim (fun h => absurd hx (not_lt_of_ge h)) id

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
⊢ comap inl (map inr g) = ⊥

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
g : Filter β
s✝ : Set α
⊢ s✝ ∈ comap inl (map inr g) ↔ s✝ ∈ ⊥
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
⊢ comap inr (map inl f) = ⊥

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
s✝ : Set β
⊢ s✝ ∈ comap inr (map inl f) ↔ s✝ ∈ ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: case inl
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ (iInf f).NeBot

Tactic:
constructor

Goal state after:
case inl
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ iInf f ≠ ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
⊢ ⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s

Tactic:
ext

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
s s✝ : Set α
⊢ s✝ ∈ ⨆ i, f i ⊓ 𝓟 s ↔ s✝ ∈ (⨆ i, f i) ⊓ 𝓟 s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B

case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p ⟨i, j⟩.fst
hj : p ⟨i, j⟩.snd
k : ι
hk : p k
ki : sa k ⊆ sa ⟨i, j⟩.fst
kj : sb k ⊆ sb ⟨i, j⟩.snd
⊢ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t

Tactic:
exact ⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
⊢ Monoid α

Tactic:
let one := e.one
  let mul := e.mul
  let pow := e.pow ℕ
  apply e.injective.monoid _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case h
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ (StrictMono fun n ↦ Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v) ∧
    ∀ (n : ℕ), P n ((fun n ↦ Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v) n)

Tactic:
constructor

Goal state after:
case h.left
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ StrictMono fun n ↦ Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v

case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
c : β
⊢ ∃ a, c ≤ f a

Tactic:
rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩
    exact ⟨g d, hcd.trans (hfg d hbd).ge⟩

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring R
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := e.addCommMonoid
⊢ ∀ (x : α), 0 • x = 0

Tactic:
simp [smul_def, zero_smul, zero_def]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
A : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
⊢ IsScalarTower R A α

Tactic:
constructor

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
A : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := ⋯
⊢ ∀ (x : R) (y : A) (z : α), (x • y) • z = x • y • z
Module: Mathlib.RingTheory.Finiteness.Defs

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
⊢ (∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) → ∃ n s, span R (range s) = N

case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG ↔ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
constructor

Goal state after:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG → ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ (∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N) → N.FG
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ range (f ∘ ULift.down) = range f

Tactic:
ext

Goal state after:
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
x✝ : M
⊢ x✝ ∈ range (f ∘ ULift.down) ↔ x✝ ∈ range f
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).FG ↔ ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).FG → ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s') → (span R s).FG
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
⊢ IsNoetherian R M ↔ WellFoundedGT { N // N.FG }

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ IsNoetherian R M → WellFoundedGT { N // N.FG }

case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ WellFoundedGT { N // N.FG } → IsNoetherian R M
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
⊢ IsNoetherian R M

Tactic:
constructor

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
H : WellFoundedGT { N // N.FG }
⊢ ∀ (s : Submodule R M), s.FG