mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
hpq : Disjoint p q
⊢ map f (p ⊓ q) = ⊥

Tactic:
disjoint_iff.mp hpq,

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
hpq : Disjoint p q
⊢ map f ⊥ = ⊥
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n = 0 ∨ a = b
⊢ n = 0 ∨ a = b

Tactic:
exact mod_cast h

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y z : R
hx : x ∈ s
hy : -y ∈ s
hz : z ∈ s
⊢ x * -y * z ∈ s

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
p : Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : InjOn ⇑f ↑p
x : M
hx : x ∈ p
y : M
hy : y ∈ p
hxy : f x = f y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝ : M
⊢ Commute (a + b) x✝

Tactic:
rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_2.mem
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝¹ x✝ : R
h✝ : x✝ ∈ ↑M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_2.zero
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ 0 ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_2.add
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure ↑M
hy✝ : y✝ ∈ AddSubmonoid.closure ↑M
a✝¹ : x✝ ∈ NonUnitalSubsemiring.closure ↑M
a✝ : y✝ ∈ NonUnitalSubsemiring.closure ↑M
⊢ x✝ + y✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
rw [List.forall_mem_cons] at HL

Goal state after:
case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
⊢ C (List.map List.prod (hd :: tl)).sum
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
rw [List.forall_mem_cons] at HL

Goal state after:
case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_1.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
· exact Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

Tactic:
refine Submodule.mem_map.trans ⟨?_, ?_⟩ <;> simp_rw [Submodule.mem_comap]

Goal state after:
case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, O.subtype y ∈ N ∧ ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y, O.subtype y ∈ N ∧ ϕ y = x
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case smul₀
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
r✝ : S
n✝ : M
mem₁✝ : r✝ ∈ s
mem₂✝ : n✝ ∈ ⊥
⊢ r✝ • n✝ ∈ ⊥

Tactic:
aesop

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

Goal state before:
pp: case smul₁
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
r✝ : R
m✝ : M
mem✝ : m✝ ∈ s • ⊥
a✝ : m✝ ∈ ⊥
⊢ r✝ • m✝ ∈ ⊥

Tactic:
aesop

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

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x m₁✝ m₂✝ : M
mem₁✝ : m₁✝ ∈ s • ⊥
mem₂✝ : m₂✝ ∈ s • ⊥
a✝¹ : m₁✝ ∈ ⊥
a✝ : m₂✝ ∈ ⊥
⊢ m₁✝ + m₂✝ ∈ ⊥

Tactic:
aesop

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

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
⊢ 0 ∈ ⊥

Tactic:
aesop

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

Goal state before:
pp: case mp.smul₀
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
r✝ : S
n✝ : M
mem₁✝ : r✝ ∈ {r}
mem₂✝ : n✝ ∈ N
⊢ ∃ m ∈ N, r✝ • n✝ = r • m

Tactic:
aesop

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ {r} • N
⊢ t • n ∈ N

Tactic:
aesop

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

Goal state before:
pp: case mpr
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ (∃ m ∈ N, x = r • m) → x ∈ {r} • N

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ x✝ ∈ ↑(p ⊔ p') ↔ x✝ ∈ ↑p + ↑p'

Tactic:
rw [SetLike.mem_coe, mem_sup, Set.mem_add]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x✝) ↔ ∃ x ∈ ↑p, ∃ y ∈ ↑p', x + y = x✝
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ ↑(p ⊔ p') = ↑p + ↑p'

Tactic:
ext
  rw [SetLike.mem_coe, mem_sup, Set.mem_add]
  simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
ha' : ∀ b ∈ s, a ≤ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Tactic:
rw [lt_iff_le_not_ge, lt_iff_le_and_ne, and_and_and_comm]

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
P : M → Prop
⊢ (∀ (x x_1 : M), x_1 ∈ p → ∀ x_2 ∈ p', x_1 + x_2 = x → P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a = b

Tactic:
rw [le_antisymm_iff, le_iff_atom_le_imp, le_iff_atom_le_imp]

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ ∀ (c : α), IsAtom c → c ≤ b → c ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
rcases isGLB_coatoms b with ⟨s, hsb, hs⟩
    rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
    · simp_all
    · exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

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

Goal state before:
pp: case mem
R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
y x✝ : A
h✝ : x✝ ∈ s
⊢ Commute x✝ x

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
⊢ Disjoint ((fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩) i) (t.sup fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩)

Tactic:
let u := (g i).map (Function.Embedding.sigmaMk i)

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk i) (g i)
⊢ Disjoint ((fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩) i) (t.sup fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
this : Disjoint (↑hs.toFinset) t → Disjoint (⨆ i ∈ hs.toFinset, f i) (⨆ i ∈ t, f i)
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι}, Disjoint (↑s₀) t → Disjoint (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀)) t
⊢ j ∉ t

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι}, Disjoint (↑s₀) t → Disjoint (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀)) t
hjt : j ∉ t
⊢ Disjoint (↑s₀) (insert j t)

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ j ∉ t ∪ ↑s₀

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : ⨆ i ∈ s, f i = ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
⊢ ∀ i_1 ∈ s, i_1 ≠ i

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
f : ι → α
s : Set ι
h₂ : ⨆ i ∈ s, f i = ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
h₁ : Disjoint (f i) (⨆ i ∈ s, f i)
⊢ False

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ (s.mulIndicator f = fun x ↦ 1) ↔ Disjoint (mulSupport f) s

Tactic:
by
  simp only [funext_iff, mulIndicator_apply_eq_one, Set.disjoint_left, mem_mulSupport,
    not_imp_not]

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
i : ι
hi : i ∈ s
⊢ (if p i then f i else 0) = f i

Tactic:
simp [h i hi]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
a : α
⊢ (∃ a_1, (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a) → ¬a = ⊥ ∧ a ∈ s

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Finset ι
f : ι → M
g : ι → N
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x) →
        (∏ x ∈ insert a s, f x, ∏ x ∈ insert a s, g x) = ∏ x ∈ insert a s, (f x, g x)

Tactic:
simp +contextual [Prod.ext_iff]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case a
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_8
inst✝ : NonAssocSemiring R
x : ι → R
x✝¹ : ι
a✝ : x✝¹ ∈ Finset.univ
x✝ : ι
⊢ Pi.single x✝¹ 1 x✝ = if x✝¹ = x✝ then 1 else 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single i m)
val✝ : Fintype ι
⊢ p f

Tactic:
rw [← Finset.univ_sum_single f]

Goal state after:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single i m)
val✝ : Fintype ι
⊢ p (∑ i, Pi.single i (f i))
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l

Tactic:
by rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
by
  induction s using Multiset.induction_on with
  | empty => simp
  | cons a s ih =>
    simp_rw [cons_add, antidiagonal_cons, ih, add_bind, bind_map, map_bind, map_map]
    congr! <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
this✝ : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
this : ¬(mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}
⊢ False

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
⊢ map f N < q

Tactic:
rwa [← comap_lt_comap_iff_of_surjective hf, comap_map_eq, sup_eq_left.mpr]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
⊢ f.ker ≤ N
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ (∃ a, a • x = ↑y) ↔ ∃ a, a • ⟨x, hx⟩ = y

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Tactic:
rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
x : α
hxs : x ∈ s
hx : x ∉ f.support
⊢ f x = 0

Tactic:
exact notMem_support_iff.1 hx

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * ∏ a ∈ f.support.erase y, g a ((erase y f) a) = g y (f y) * ∏ x ∈ f.support.erase y, g x (f x)

Tactic:
Finset.prod_congr rfl

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * (f.support.erase y).prod ?m.68 = g y (f y) * ∏ x ∈ f.support.erase y, g x (f x)

α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = ?m.68 x

α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ α → N
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
h : IsLeftRegular (abv 1)
⊢ (fun x ↦ abv 1 * x) (abv 1) = (fun x ↦ abv 1 * x) 1

Tactic:
by simp [← abv.map_mul]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support

Tactic:
exact mod_cast h

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
hb : b ∉ Set.range ⇑f
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Tactic:
replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb

Goal state after:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range ⇑f
hg : g b = 0
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case ha
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ 0 ≤ g i

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h0
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
j : ι
hj : j ∈ s \ {i}
⊢ g j ≤ f j

Tactic:
aesop

Goal state after: